From d454617d4c502a34d4eec5611a0049e3aa47fbe9 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 30 May 2026 17:22:54 +0000 Subject: [PATCH 01/26] cterm/symbolic, kcfg/explore, tests/unit/cterm/test_symbolic: surface 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 (cherry picked from commit d4e9cb3966d821f3a422cfd1eb09e5c6769915a6) --- pyk/src/pyk/cterm/symbolic.py | 12 +- pyk/src/pyk/kcfg/explore.py | 7 +- pyk/src/tests/unit/cterm/test_symbolic.py | 183 ++++++++++++++++++++++ 3 files changed, 200 insertions(+), 2 deletions(-) create mode 100644 pyk/src/tests/unit/cterm/test_symbolic.py diff --git a/pyk/src/pyk/cterm/symbolic.py b/pyk/src/pyk/cterm/symbolic.py index af8f9a4e36..906b7f6c6f 100644 --- a/pyk/src/pyk/cterm/symbolic.py +++ b/pyk/src/pyk/cterm/symbolic.py @@ -70,6 +70,7 @@ class CTermExecute(NamedTuple): next_states: tuple[NextState, ...] depth: int vacuous: bool + aborted: bool logs: tuple[LogEntry, ...] @@ -162,6 +163,7 @@ def execute( module_name: str | None = None, booster_only_simplify: bool | None = None, haskell_logging: bool | None = None, + raise_on_aborted: bool = True, ) -> CTermExecute: _LOGGER.debug(f'Executing: {cterm}') @@ -184,7 +186,14 @@ def execute( raise self._smt_solver_error(err) from err self._capture_haskell_log(response.haskell_log_entries) - if isinstance(response, AbortedResult): + # Under booster-only execution, an `AbortedResult` is the expected signal that the booster + # could make no further progress (it is what drives the recover-mode ladder). Callers that + # want to inspect the abort rather than treat it as fatal pass `raise_on_aborted=False`; the + # `AbortedResult.reason`/`next_states` class attributes let the rest of this body proceed + # unchanged, surfacing `aborted=True` on the result. + aborted = isinstance(response, AbortedResult) + if aborted and raise_on_aborted: + assert isinstance(response, AbortedResult) unknown_predicate = response.unknown_predicate.text if response.unknown_predicate else None raise ValueError(f'Backend responded with aborted state. Unknown predicate: {unknown_predicate}') @@ -207,6 +216,7 @@ def execute( next_states=next_states, depth=response.depth, vacuous=response.reason is StopReason.VACUOUS, + aborted=aborted, logs=response.logs, ) diff --git a/pyk/src/pyk/kcfg/explore.py b/pyk/src/pyk/kcfg/explore.py index 1eef51588a..f2060f5fb9 100644 --- a/pyk/src/pyk/kcfg/explore.py +++ b/pyk/src/pyk/kcfg/explore.py @@ -229,7 +229,7 @@ def extend_cterm( if _cterm != abstract_cterm: return [Abstract(abstract_cterm)] - cterm, next_states, depth, vacuous, next_node_logs = self.cterm_symbolic.execute( + exec_result = self.cterm_symbolic.execute( _cterm, depth=execute_depth, cut_point_rules=cut_point_rules, @@ -237,6 +237,11 @@ def extend_cterm( module_name=module_name, haskell_logging=haskell_logging, ) + cterm = exec_result.state + next_states = exec_result.next_states + depth = exec_result.depth + vacuous = exec_result.vacuous + next_node_logs = exec_result.logs extend_results: list[KCFGExtendResult] = [] diff --git a/pyk/src/tests/unit/cterm/test_symbolic.py b/pyk/src/tests/unit/cterm/test_symbolic.py new file mode 100644 index 0000000000..569928b5ba --- /dev/null +++ b/pyk/src/tests/unit/cterm/test_symbolic.py @@ -0,0 +1,183 @@ +from __future__ import annotations + +import json +from typing import TYPE_CHECKING +from unittest.mock import Mock, patch + +import pytest + +from pyk.cterm.symbolic import HASKELL_LOGGING_ENTRIES, CTermSymbolic, cterm_symbolic +from pyk.kast.prelude.ml import mlTop +from pyk.kore.prelude import int_dv +from pyk.kore.rpc import AbortedResult, State, StuckResult + +if TYPE_CHECKING: + from pathlib import Path + + from pyk.cterm import CTerm + + +def _mock_client_cts(response: object) -> tuple[Mock, CTermSymbolic]: + """Build a `CTermSymbolic` whose backend returns ``response`` and whose Kast<->Kore + conversions are stubbed, returning the backend `Mock` so a test can inspect call args. + """ + kore_client = Mock() + kore_client.execute.return_value = response + cts = CTermSymbolic(kore_client, Mock()) + cts.kast_to_kore = Mock(return_value=Mock()) # type: ignore[method-assign] + cts.kore_to_kast = Mock(return_value=mlTop()) # type: ignore[method-assign] + return kore_client, cts + + +def _cterm_symbolic(response: object) -> CTermSymbolic: + """Build a `CTermSymbolic` whose backend returns ``response`` and whose Kast<->Kore + conversions are stubbed, so ``execute`` can be exercised without a real ``KDefinition``. + """ + kore_client = Mock() + kore_client.execute.return_value = response + cts = CTermSymbolic(kore_client, Mock()) + # The conversions need a real definition; stub them. ``kore_to_kast`` returns ML-top so + # ``CTerm.from_kast`` yields ``CTerm.top()`` (no config cell required). + cts.kast_to_kore = Mock(return_value=Mock()) # type: ignore[method-assign] + cts.kore_to_kast = Mock(return_value=mlTop()) # type: ignore[method-assign] + return cts + + +def test_execute_on_requests_configured_entries() -> None: + # Given + kore_client, cts = _mock_client_cts(StuckResult(state=State(term=int_dv(2)), depth=1, logs=())) + dummy: CTerm = Mock() + + # When the per-call flag turns logging on + cts.execute(dummy, haskell_logging=True) + + # Then the configured entry set (the canonical default here) is what reaches KoreClient.execute + _args, kwargs = kore_client.execute.call_args + assert kwargs['haskell_logging'] == HASKELL_LOGGING_ENTRIES + + +def test_execute_honors_custom_entry_set() -> None: + # Given a CTermSymbolic configured with a custom entry set + kore_client = Mock() + kore_client.execute.return_value = StuckResult(state=State(term=int_dv(2)), depth=1, logs=()) + cts = CTermSymbolic(kore_client, Mock(), haskell_log_entries=['Rewrite', 'DebugApplyEquation']) + cts.kast_to_kore = Mock(return_value=Mock()) # type: ignore[method-assign] + cts.kore_to_kast = Mock(return_value=mlTop()) # type: ignore[method-assign] + + # When + cts.execute(Mock(), haskell_logging=True) + + # Then exactly that set is requested + _args, kwargs = kore_client.execute.call_args + assert kwargs['haskell_logging'] == ('Rewrite', 'DebugApplyEquation') + + +def test_execute_default_leaves_haskell_logging_off() -> None: + # Given + kore_client, cts = _mock_client_cts(StuckResult(state=State(term=int_dv(2)), depth=1, logs=())) + dummy: CTerm = Mock() + + # When called with defaults + cts.execute(dummy) + + # Then logging is left untouched (None preserves today's behaviour) + _args, kwargs = kore_client.execute.call_args + assert kwargs['haskell_logging'] is None + + +def _log_dir_cts(response: object, haskell_log_dir: Path) -> tuple[Mock, CTermSymbolic]: + kore_client = Mock() + kore_client.execute.return_value = response + cts = CTermSymbolic(kore_client, Mock(), haskell_log_dir=haskell_log_dir) + cts.kast_to_kore = Mock(return_value=Mock()) # type: ignore[method-assign] + cts.kore_to_kast = Mock(return_value=mlTop()) # type: ignore[method-assign] + return kore_client, cts + + +def test_execute_writes_haskell_log_bundle(tmp_path: Path) -> None: + # Given a configured log dir and a response carrying a per-request bundle + entry = {'context': ['Proxy'], 'message': 'simplifying'} + response = StuckResult(state=State(term=int_dv(2)), depth=1, logs=(), haskell_log_entries=(entry,)) + kore_client, cts = _log_dir_cts(response, tmp_path) + kore_client.last_request_id = 'proof-007' + + # When + cts.execute(Mock()) + + # Then logging is requested and the bundle lands in /.jsonl, one JSON value per line + _args, kwargs = kore_client.execute.call_args + assert kwargs['haskell_logging'] == HASKELL_LOGGING_ENTRIES + log_file = tmp_path / 'proof-007.jsonl' + assert json.loads(log_file.read_text().strip()) == entry + + +def test_execute_writes_no_file_when_bundle_absent(tmp_path: Path) -> None: + # Given a configured log dir but a response with no bundle + response = StuckResult(state=State(term=int_dv(2)), depth=1, logs=(), haskell_log_entries=None) + kore_client, cts = _log_dir_cts(response, tmp_path) + kore_client.last_request_id = 'proof-008' + + # When + cts.execute(Mock()) + + # Then nothing is written + assert not list(tmp_path.iterdir()) + + +def test_cterm_symbolic_forwards_custom_entry_set() -> None: + # Given a caller that overrides the per-request entry set through the factory + with patch('pyk.cterm.symbolic.KoreClient'): + with cterm_symbolic( + definition=Mock(), + definition_dir=Mock(), + start_server=False, + port=1, + haskell_log_entries=['Rewrite', 'DebugApplyEquation'], + ) as cts: + # Then the built CTermSymbolic requests exactly that set + assert cts._haskell_log_entries == ('Rewrite', 'DebugApplyEquation') + + +def test_cterm_symbolic_defaults_to_canonical_entry_set() -> None: + # Given no override + with patch('pyk.cterm.symbolic.KoreClient'): + with cterm_symbolic(definition=Mock(), definition_dir=Mock(), start_server=False, port=1) as cts: + # Then the canonical default is used + assert cts._haskell_log_entries == HASKELL_LOGGING_ENTRIES + + +def test_execute_raises_on_abort_by_default() -> None: + # Given + cts = _cterm_symbolic(AbortedResult(state=State(term=int_dv(1)), depth=0, unknown_predicate=None, logs=())) + dummy: CTerm = Mock() + + # Then + with pytest.raises(ValueError, match='aborted state'): + cts.execute(dummy) + + +def test_execute_surfaces_abort_when_not_raising() -> None: + # Given + cts = _cterm_symbolic(AbortedResult(state=State(term=int_dv(1)), depth=3, unknown_predicate=None, logs=())) + dummy: CTerm = Mock() + + # When + result = cts.execute(dummy, raise_on_aborted=False) + + # Then + assert result.aborted + assert result.depth == 3 + assert not result.vacuous + + +def test_execute_not_aborted_on_normal_result() -> None: + # Given + cts = _cterm_symbolic(StuckResult(state=State(term=int_dv(2)), depth=1, logs=())) + dummy: CTerm = Mock() + + # When + result = cts.execute(dummy, raise_on_aborted=False) + + # Then + assert not result.aborted + assert result.depth == 1 From abed03cd9b849ab7eba64cb94f878c150172edf2 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 30 May 2026 17:35:30 +0000 Subject: [PATCH 02/26] kore/rpc, cterm/symbolic, tests/unit/{kore/test_client,cterm/test_symbolic}: add indeterminate to ImpliesResult and CTermImplies MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 (cherry picked from commit 0c7c26b83ae9218557b7017c412cf96bd08bed5f) --- pyk/src/pyk/cterm/symbolic.py | 5 ++-- pyk/src/pyk/kore/rpc.py | 5 ++++ pyk/src/tests/unit/cterm/test_symbolic.py | 28 ++++++++++++++++++++++- pyk/src/tests/unit/kore/test_client.py | 19 +++++++++++++++ 4 files changed, 54 insertions(+), 3 deletions(-) diff --git a/pyk/src/pyk/cterm/symbolic.py b/pyk/src/pyk/cterm/symbolic.py index 906b7f6c6f..967194cca9 100644 --- a/pyk/src/pyk/cterm/symbolic.py +++ b/pyk/src/pyk/cterm/symbolic.py @@ -79,6 +79,7 @@ class CTermImplies(NamedTuple): failing_cells: tuple[tuple[str, KInner], ...] remaining_implication: KInner | None logs: tuple[LogEntry, ...] + indeterminate: bool | None = None @final @@ -371,7 +372,7 @@ def implies( ) ) remaining_implication = CTerm._ml_impl(antecedent.constraints, consequent_constraints) - return CTermImplies(None, tuple(failing_cells), remaining_implication, result.logs) + return CTermImplies(None, tuple(failing_cells), remaining_implication, result.logs, result.indeterminate) if result.substitution is None: raise ValueError('Received empty substutition for valid implication.') @@ -381,7 +382,7 @@ def implies( ml_pred = self.kore_to_kast(result.predicate) ml_subst_pred = mlAnd(flatten_label('#And', ml_subst) + flatten_label('#And', ml_pred)) csubst = CSubst.from_pred(ml_subst_pred) - return CTermImplies(csubst, (), None, result.logs) + return CTermImplies(csubst, (), None, result.logs, result.indeterminate) def assume_defined( self, cterm: CTerm, module_name: str | None = None, booster_only_simplify: bool = False diff --git a/pyk/src/pyk/kore/rpc.py b/pyk/src/pyk/kore/rpc.py index e4e0355883..14eb642189 100644 --- a/pyk/src/pyk/kore/rpc.py +++ b/pyk/src/pyk/kore/rpc.py @@ -895,6 +895,10 @@ class ImpliesResult: predicate: Pattern | None logs: tuple[LogEntry, ...] haskell_log_entries: tuple[Any, ...] | None = None + # `Just True` only on booster's MatchIndeterminate-no-progress paths; absent (⇒ None) on + # every decisive `valid` verdict and every error. Lets a caller tell a decisive invalid + # (trust) from a couldn't-determine (escalate to kore). See booster `f911be4e0`. + indeterminate: bool | None = None @staticmethod def from_dict(dct: Mapping[str, Any]) -> ImpliesResult: @@ -908,6 +912,7 @@ def from_dict(dct: Mapping[str, Any]) -> ImpliesResult: predicate=kore_term(predicate) if predicate is not None else None, logs=logs, haskell_log_entries=_parse_haskell_log_entries(dct), + indeterminate=dct.get('indeterminate'), ) diff --git a/pyk/src/tests/unit/cterm/test_symbolic.py b/pyk/src/tests/unit/cterm/test_symbolic.py index 569928b5ba..737b3f4dd1 100644 --- a/pyk/src/tests/unit/cterm/test_symbolic.py +++ b/pyk/src/tests/unit/cterm/test_symbolic.py @@ -9,7 +9,7 @@ from pyk.cterm.symbolic import HASKELL_LOGGING_ENTRIES, CTermSymbolic, cterm_symbolic from pyk.kast.prelude.ml import mlTop from pyk.kore.prelude import int_dv -from pyk.kore.rpc import AbortedResult, State, StuckResult +from pyk.kore.rpc import AbortedResult, ImpliesResult, State, StuckResult if TYPE_CHECKING: from pathlib import Path @@ -181,3 +181,29 @@ def test_execute_not_aborted_on_normal_result() -> None: # Then assert not result.aborted assert result.depth == 1 + + +@pytest.mark.parametrize('indeterminate', [True, False, None], ids=['true', 'false', 'absent']) +def test_implies_surfaces_indeterminate(indeterminate: bool | None) -> None: + # Given a falsifiable implication carrying the backend `indeterminate` flag + kore_client = Mock() + kore_client.implies.return_value = ImpliesResult( + valid=False, + implication=Mock(), + substitution=None, + predicate=None, + logs=(), + indeterminate=indeterminate, + ) + cts = CTermSymbolic(kore_client, Mock()) + cts.kast_to_kore = Mock(return_value=Mock()) # type: ignore[method-assign] + # Stub CTerm operands: no free vars (so no consequent binding), arbitrary kast. + antecedent: CTerm = Mock(free_vars=frozenset()) + consequent: CTerm = Mock(free_vars=frozenset()) + + # When + result = cts.implies(antecedent, consequent) + + # Then + assert result.csubst is None + assert result.indeterminate is indeterminate diff --git a/pyk/src/tests/unit/kore/test_client.py b/pyk/src/tests/unit/kore/test_client.py index e93e4558c2..ff9413477a 100644 --- a/pyk/src/tests/unit/kore/test_client.py +++ b/pyk/src/tests/unit/kore/test_client.py @@ -205,6 +205,25 @@ def test_implies( assert actual == expected +@pytest.mark.parametrize('indeterminate', [True, False, None], ids=['true', 'false', 'absent']) +def test_implies_parses_indeterminate( + kore_client: KoreClient, + rpc_client: MockClient, + indeterminate: bool | None, +) -> None: + # Given a falsifiable implication whose `indeterminate` flag varies (absent ⇒ omitted) + response: dict[str, Any] = {'valid': False, 'implication': kore(int_top)} + if indeterminate is not None: + response['indeterminate'] = indeterminate + rpc_client.assume_response(response) + + # When + actual = kore_client.implies(int_bottom, int_top) + + # Then + assert actual.indeterminate is indeterminate + + SIMPLIFY_TEST_DATA: Final = ( ( And(INT, (int_top, int_top)), From 1c5cd132ee71835e474de4e9e0533244e3f56795 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 3 Jun 2026 17:19:00 +0000 Subject: [PATCH 03/26] cterm/symbolic, tests/unit/cterm/test_symbolic: thread haskell_logging 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 (cherry picked from commit 4a3b142c80cd552a5df4961f1470d873fa83a84d) --- pyk/src/pyk/cterm/symbolic.py | 1 + pyk/src/tests/unit/cterm/test_symbolic.py | 27 +++++++++++++++++++++++ 2 files changed, 28 insertions(+) diff --git a/pyk/src/pyk/cterm/symbolic.py b/pyk/src/pyk/cterm/symbolic.py index 967194cca9..abbcadd0fa 100644 --- a/pyk/src/pyk/cterm/symbolic.py +++ b/pyk/src/pyk/cterm/symbolic.py @@ -165,6 +165,7 @@ def execute( booster_only_simplify: bool | None = None, haskell_logging: bool | None = None, raise_on_aborted: bool = True, + haskell_logging: bool | None = None, ) -> CTermExecute: _LOGGER.debug(f'Executing: {cterm}') diff --git a/pyk/src/tests/unit/cterm/test_symbolic.py b/pyk/src/tests/unit/cterm/test_symbolic.py index 737b3f4dd1..1eeeb6e43d 100644 --- a/pyk/src/tests/unit/cterm/test_symbolic.py +++ b/pyk/src/tests/unit/cterm/test_symbolic.py @@ -183,6 +183,33 @@ def test_execute_not_aborted_on_normal_result() -> None: assert result.depth == 1 +def test_execute_forwards_per_call_params() -> None: + # Given + kore_client, cts = _mock_client_cts(StuckResult(state=State(term=int_dv(2)), depth=1, logs=())) + + # When + cts.execute(Mock(), booster_only_simplify=True, haskell_logging=True) + + # Then the per-call flags reach the underlying KoreClient.execute; the haskell_logging bool is + # resolved to the configured entry set on the way through. + _args, kwargs = kore_client.execute.call_args + assert kwargs['booster_only_simplify'] is True + assert kwargs['haskell_logging'] == HASKELL_LOGGING_ENTRIES + + +def test_execute_default_params_preserve_current_call() -> None: + # Given + kore_client, cts = _mock_client_cts(StuckResult(state=State(term=int_dv(2)), depth=1, logs=())) + + # When called with defaults + cts.execute(Mock()) + + # Then booster-only falls back to the instance default (False) and logging is off + _args, kwargs = kore_client.execute.call_args + assert kwargs['booster_only_simplify'] is False + assert kwargs['haskell_logging'] is None + + @pytest.mark.parametrize('indeterminate', [True, False, None], ids=['true', 'false', 'absent']) def test_implies_surfaces_indeterminate(indeterminate: bool | None) -> None: # Given a falsifiable implication carrying the backend `indeterminate` flag From 11ca61c5d08e922cc38cd0faf1c0bdfe986a2ae7 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 3 Jun 2026 17:19:16 +0000 Subject: [PATCH 04/26] kcfg/explore, tests/unit/cterm/test_symbolic: thread booster_only_simplify/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 (cherry picked from commit 111113b034d9baaa68d21b09383076fffaa3d005) --- pyk/src/pyk/kcfg/explore.py | 4 ++++ pyk/src/tests/unit/cterm/test_symbolic.py | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/pyk/src/pyk/kcfg/explore.py b/pyk/src/pyk/kcfg/explore.py index f2060f5fb9..9ca3a84456 100644 --- a/pyk/src/pyk/kcfg/explore.py +++ b/pyk/src/pyk/kcfg/explore.py @@ -218,6 +218,8 @@ def extend_cterm( cut_point_rules: Iterable[str] = (), terminal_rules: Iterable[str] = (), module_name: str | None = None, + booster_only_simplify: bool | None = None, + raise_on_aborted: bool = True, haskell_logging: bool | None = None, ) -> list[KCFGExtendResult]: @@ -235,6 +237,8 @@ def extend_cterm( cut_point_rules=cut_point_rules, terminal_rules=terminal_rules, module_name=module_name, + booster_only_simplify=booster_only_simplify, + raise_on_aborted=raise_on_aborted, haskell_logging=haskell_logging, ) cterm = exec_result.state diff --git a/pyk/src/tests/unit/cterm/test_symbolic.py b/pyk/src/tests/unit/cterm/test_symbolic.py index 1eeeb6e43d..9fd10c4143 100644 --- a/pyk/src/tests/unit/cterm/test_symbolic.py +++ b/pyk/src/tests/unit/cterm/test_symbolic.py @@ -188,7 +188,7 @@ def test_execute_forwards_per_call_params() -> None: kore_client, cts = _mock_client_cts(StuckResult(state=State(term=int_dv(2)), depth=1, logs=())) # When - cts.execute(Mock(), booster_only_simplify=True, haskell_logging=True) + cts.execute(Mock(), booster_only_simplify=True, haskell_logging=True, raise_on_aborted=False) # Then the per-call flags reach the underlying KoreClient.execute; the haskell_logging bool is # resolved to the configured entry set on the way through. From 00d9cd1e4701930e9d9dd3a2f7b21eb72cb64fb9 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 30 May 2026 17:43:41 +0000 Subject: [PATCH 05/26] kcfg/{kcfg,explore}, proof/reachability, tests/unit/{test_proof,kcfg/test_explore}: move the stuck judgment from extend_cterm into commit MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `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 (cherry picked from commit 80b0a4aecd3eb0d47eace790c666e610958a898b) --- pyk/src/pyk/kcfg/explore.py | 8 +++-- pyk/src/pyk/kcfg/kcfg.py | 11 +++++++ pyk/src/pyk/proof/reachability.py | 24 ++++++++++++++ pyk/src/tests/unit/kcfg/test_explore.py | 43 +++++++++++++++++++++++++ pyk/src/tests/unit/test_proof.py | 18 ++++++++++- 5 files changed, 100 insertions(+), 4 deletions(-) create mode 100644 pyk/src/tests/unit/kcfg/test_explore.py diff --git a/pyk/src/pyk/kcfg/explore.py b/pyk/src/pyk/kcfg/explore.py index 9ca3a84456..07704f57fb 100644 --- a/pyk/src/pyk/kcfg/explore.py +++ b/pyk/src/pyk/kcfg/explore.py @@ -17,7 +17,7 @@ from ..kast.pretty import PrettyPrinter from ..kore.rpc import LogRewrite, RewriteSuccess from ..utils import not_none, shorten_hashes, single, unique -from .kcfg import KCFG, Abstract, Branch, NDBranch, Step, Stuck, Vacuous +from .kcfg import KCFG, Abstract, Branch, NDBranch, NoProgress, Step, Vacuous from .semantics import DefaultSemantics if TYPE_CHECKING: @@ -253,12 +253,14 @@ def extend_cterm( if depth > 0: extend_results.append(Step(cterm, depth, next_node_logs, self._extract_rule_labels(next_node_logs))) - # Stuck or vacuous + # No-progress or vacuous. `Vacuous` is a context-free semantic verdict and stays here; a + # depth-0 no-progress result is reported as the neutral `NoProgress` rather than `Stuck`, so + # the coordinator (`APRProof.commit`) decides whether the node is terminal (see C6). if not next_states: if vacuous: extend_results.append(Vacuous()) elif depth == 0: - extend_results.append(Stuck()) + extend_results.append(NoProgress()) # Cut rule elif len(next_states) == 1: if not self.kcfg_semantics.can_make_custom_step(cterm): diff --git a/pyk/src/pyk/kcfg/kcfg.py b/pyk/src/pyk/kcfg/kcfg.py index 35482b149c..20268b2376 100644 --- a/pyk/src/pyk/kcfg/kcfg.py +++ b/pyk/src/pyk/kcfg/kcfg.py @@ -1320,6 +1320,17 @@ class Vacuous(KCFGExtendResult): ... class Stuck(KCFGExtendResult): ... +@final +@dataclass(frozen=True) +class NoProgress(KCFGExtendResult): + """The backend made no progress on a node, without judging it stuck. + + Emitted by ``KCFGExplore.extend_cterm`` in place of ``Stuck`` so the *decision* of whether a + no-progress node is terminal stays with the proof coordinator (``APRProof.commit``), which has + the full node context. Never applied by ``KCFG.extend`` — the coordinator intercepts it. + """ + + @final @dataclass(frozen=True) class Abstract(KCFGExtendResult): diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 0b4a66d2b3..e7c0fb14cb 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -13,6 +13,7 @@ from ..kast.prelude.ml import mlAnd, mlTop from ..kcfg import KCFG, KCFGStore from ..kcfg.exploration import KCFGExploration +from ..kcfg.kcfg import NoProgress from ..kore.rpc import LogEntry, client_label from ..ktool.claim_index import ClaimIndex from ..utils import FrozenDict, ensure_dir_path, hash_str, shorten_hashes, single @@ -75,6 +76,15 @@ class APRProofTerminalResult(APRProofResult): ... class APRProofBoundedResult(APRProofResult): ... +@dataclass +class APRProofStuckResult(APRProofResult): + """The backend reported no progress; the coordinator (`commit`) is to mark the node stuck. + + Carrying this as a distinct result — rather than a `Stuck` extension applied by `KCFG.extend` — + keeps `add_stuck` solely in `commit`, where the full node context lives (see C6). + """ + + @dataclass(frozen=True) class APRProofStep: node: KCFG.Node @@ -240,6 +250,10 @@ def commit(self, result: APRProofResult) -> None: self.kcfg.create_cover(result.node_id, self.target, csubst=result.csubst) elif isinstance(result, APRProofTerminalResult): self.add_terminal(result.node_id) + elif isinstance(result, APRProofStuckResult): + # Sole site that marks a node stuck: the coordinator owns this judgment (C6). + _LOGGER.info(f'Stuck node {self.id}: {result.node_id}') + self.kcfg.add_stuck(result.node_id) elif isinstance(result, APRProofBoundedResult): self.add_bounded(result.node_id) else: @@ -896,6 +910,16 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: # We can obtain two results at most assert len(extend_results) <= 2 + # A no-progress result is not applied to the KCFG by the worker; the coordinator decides + # the node is stuck (sole `add_stuck` site is `commit`, see C6). + if len(extend_results) == 1 and isinstance(extend_results[0], NoProgress): + return [ + APRProofStuckResult( + node_id=step.node.id, + optimize_kcfg=self.optimize_kcfg, + prior_loops_cache_update=prior_loops, + ) + ] # We have obtained two results: first is to be applied, second to be cached potentially if len(extend_results) == 2: # Cache only if the current node is at non-zero depth diff --git a/pyk/src/tests/unit/kcfg/test_explore.py b/pyk/src/tests/unit/kcfg/test_explore.py new file mode 100644 index 0000000000..b3dd9e8cc7 --- /dev/null +++ b/pyk/src/tests/unit/kcfg/test_explore.py @@ -0,0 +1,43 @@ +from __future__ import annotations + +from unittest.mock import Mock + +from pyk.cterm.symbolic import CTermExecute +from pyk.kcfg.explore import KCFGExplore +from pyk.kcfg.kcfg import NoProgress, Step + +from ..test_kcfg import term + + +def _explore(exec_result: CTermExecute) -> KCFGExplore: + cterm_symbolic = Mock() + cterm_symbolic.execute.return_value = exec_result + # DefaultSemantics: custom_step → None, abstract_node → identity, so extend_cterm reaches execute. + return KCFGExplore(cterm_symbolic) + + +def test_extend_cterm_reports_no_progress_not_stuck() -> None: + # Given a backend that makes no progress (depth 0, no next states, not vacuous) + cterm = term(1) + explore = _explore(CTermExecute(state=cterm, next_states=(), depth=0, vacuous=False, aborted=False, logs=())) + + # When + results = explore.extend_cterm(cterm, node_id=1) + + # Then the worker emits the neutral NoProgress signal — never Stuck (the coordinator decides) + assert len(results) == 1 + assert isinstance(results[0], NoProgress) + + +def test_extend_cterm_step_on_progress() -> None: + # Given a backend that makes progress + cterm = term(1) + nxt = term(2) + explore = _explore(CTermExecute(state=nxt, next_states=(), depth=3, vacuous=False, aborted=False, logs=())) + + # When + results = explore.extend_cterm(cterm, node_id=1) + + # Then a basic-block Step is produced (unchanged behaviour) + assert len(results) == 1 + assert isinstance(results[0], Step) diff --git a/pyk/src/tests/unit/test_proof.py b/pyk/src/tests/unit/test_proof.py index f28b292d21..67a6a84e38 100644 --- a/pyk/src/tests/unit/test_proof.py +++ b/pyk/src/tests/unit/test_proof.py @@ -11,7 +11,7 @@ from pyk.proof import EqualityProof from pyk.proof.implies import EqualitySummary from pyk.proof.proof import CompositeSummary, Proof, ProofStatus -from pyk.proof.reachability import APRFailureInfo, APRProof, APRSummary +from pyk.proof.reachability import APRFailureInfo, APRProof, APRProofStuckResult, APRSummary from .kcfg.test_minimize import minimization_test_kcfg from .test_kcfg import node, node_dicts, term @@ -238,6 +238,22 @@ def test_apr_proof_from_dict_heterogeneous_subproofs(proof_dir: Path) -> None: assert proof.dict == proof_from_disk.dict +def test_commit_stuck_result_marks_node_stuck() -> None: + # Given a proof with a pending leaf node that is neither init nor target + kcfg = KCFG() + n1 = kcfg.create_node(term(1)) + n2 = kcfg.create_node(term(2)) + n3 = kcfg.create_node(term(3)) + proof = APRProof(id='stuck_proof', kcfg=kcfg, terminal=[], init=n1.id, target=n2.id, logs={}) + assert not kcfg.is_stuck(n3.id) + + # When the coordinator commits a no-progress (stuck) result for that node + proof.commit(APRProofStuckResult(node_id=n3.id, prior_loops_cache_update=(), optimize_kcfg=False)) + + # Then the node is marked stuck — `commit` is the sole `add_stuck` site (C6) + assert kcfg.is_stuck(n3.id) + + def test_apr_proof_minimization_and_terminals() -> None: # 25 /-- X >=Int 5 --> 10 # 5 10 15 20 /-- X >=Int 0 --> 6 --> 8 From a4de35e1bce31ff6ae6b40022f112554b344a754 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 30 May 2026 17:48:29 +0000 Subject: [PATCH 06/26] proof/reachability, tests/unit/test_proof: _check_subsume returns a tagged outcome, thread booster_only MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 (cherry picked from commit b28db83e528d8d90d09e890e5791e156b9c97f40) --- pyk/src/pyk/proof/reachability.py | 56 +++++++++++++++++++++----- pyk/src/tests/unit/test_proof.py | 66 ++++++++++++++++++++++++++++++- 2 files changed, 111 insertions(+), 11 deletions(-) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index e7c0fb14cb..7be092d001 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -3,8 +3,9 @@ import json import logging import re +from abc import ABC from dataclasses import dataclass, field -from typing import TYPE_CHECKING +from typing import TYPE_CHECKING, final from ..cterm.cterm import remove_useless_constraints from ..kast.inner import KInner, Subst @@ -85,6 +86,31 @@ class APRProofStuckResult(APRProofResult): """ +class SubsumptionCheck(ABC): + """Tagged outcome of a subsumption (`implies`) check, replacing a bare ``CSubst | None``. + + Distinguishes a decisive non-subsumption (``DecisiveInvalid`` — trust it) from a + couldn't-determine (``Indeterminate`` — recover-mode escalates to a kore implies). Today both + map to "proceed to execute", identical to the old ``csubst is None`` (see C7). + """ + + +@final +@dataclass(frozen=True) +class Subsumed(SubsumptionCheck): + csubst: CSubst + + +@final +@dataclass(frozen=True) +class DecisiveInvalid(SubsumptionCheck): ... + + +@final +@dataclass(frozen=True) +class Indeterminate(SubsumptionCheck): ... + + @dataclass(frozen=True) class APRProofStep: node: KCFG.Node @@ -812,17 +838,27 @@ def _may_subsume(self, node: KCFG.Node, target_node: KCFG.Node) -> bool: return False return True - def _check_subsume(self, node: KCFG.Node, target_node: KCFG.Node, proof_id: str) -> CSubst | None: + def _check_subsume( + self, + node: KCFG.Node, + target_node: KCFG.Node, + proof_id: str, + booster_only: bool | None = None, + ) -> SubsumptionCheck: target_cterm = target_node.cterm _LOGGER.debug(f'Checking subsumption into target state {proof_id}: {shorten_hashes((node.id, target_cterm))}') if self.fast_check_subsumption and not self._may_subsume(node, target_node): _LOGGER.info(f'Skipping full subsumption check because of fast may subsume check {proof_id}: {node.id}') - return None - _csubst = self.kcfg_explore.cterm_symbolic.implies(node.cterm, target_cterm, assume_defined=self.assume_defined) - csubst = _csubst.csubst - if csubst is not None: + return DecisiveInvalid() + result = self.kcfg_explore.cterm_symbolic.implies( + node.cterm, target_cterm, assume_defined=self.assume_defined, booster_only_simplify=booster_only + ) + if result.csubst is not None: _LOGGER.info(f'Subsumed into target node {proof_id}: {shorten_hashes((node.id, target_node.id))}') - return csubst + return Subsumed(result.csubst) + # Not subsumed: a decisive invalid is trusted; a couldn't-determine (booster + # `MatchIndeterminate`) is surfaced so recover-mode can escalate to a kore implies (C13). + return Indeterminate() if result.indeterminate else DecisiveInvalid() def step_proof(self, step: APRProofStep) -> list[APRProofResult]: # Check if the current node should be bounded @@ -860,13 +896,13 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: # Subsumption is checked if and only if the target node # and the current node are either both terminal or both not terminal if is_terminal == target_is_terminal: - csubst = self._check_subsume(step.node, step.target, proof_id=step.proof_id) - if csubst is not None: + subsumption = self._check_subsume(step.node, step.target, proof_id=step.proof_id) + if isinstance(subsumption, Subsumed): # Information about the subsumed node being terminal must be returned # so that the set of terminal nodes is correctly updated return terminal_result + [ APRProofSubsumeResult( - csubst=csubst, + csubst=subsumption.csubst, optimize_kcfg=self.optimize_kcfg, node_id=step.node.id, prior_loops_cache_update=prior_loops, diff --git a/pyk/src/tests/unit/test_proof.py b/pyk/src/tests/unit/test_proof.py index 67a6a84e38..50929f91d8 100644 --- a/pyk/src/tests/unit/test_proof.py +++ b/pyk/src/tests/unit/test_proof.py @@ -1,9 +1,12 @@ from __future__ import annotations from typing import TYPE_CHECKING +from unittest.mock import Mock import pytest +from pyk.cterm import CSubst +from pyk.cterm.symbolic import CTermImplies from pyk.kast.prelude.kbool import BOOL from pyk.kast.prelude.kint import intToken from pyk.kcfg.exploration import KCFGExplorationNodeAttr @@ -11,7 +14,16 @@ from pyk.proof import EqualityProof from pyk.proof.implies import EqualitySummary from pyk.proof.proof import CompositeSummary, Proof, ProofStatus -from pyk.proof.reachability import APRFailureInfo, APRProof, APRProofStuckResult, APRSummary +from pyk.proof.reachability import ( + APRFailureInfo, + APRProof, + APRProofStuckResult, + APRProver, + APRSummary, + DecisiveInvalid, + Indeterminate, + Subsumed, +) from .kcfg.test_minimize import minimization_test_kcfg from .test_kcfg import node, node_dicts, term @@ -22,6 +34,8 @@ from pytest import TempPathFactory + from pyk.proof.reachability import SubsumptionCheck + @pytest.fixture(scope='function') def proof_dir(tmp_path_factory: TempPathFactory) -> Path: @@ -254,6 +268,56 @@ def test_commit_stuck_result_marks_node_stuck() -> None: assert kcfg.is_stuck(n3.id) +_CSUBST_SENTINEL: Final = CSubst() + +_CHECK_SUBSUME_DATA: Final = ( + ('subsumed', _CSUBST_SENTINEL, None, Subsumed), + ('decisive-invalid', None, False, DecisiveInvalid), + ('decisive-invalid-absent', None, None, DecisiveInvalid), + ('indeterminate', None, True, Indeterminate), +) + + +@pytest.mark.parametrize( + 'test_id,csubst,indeterminate,expected', + _CHECK_SUBSUME_DATA, + ids=[d[0] for d in _CHECK_SUBSUME_DATA], +) +def test_check_subsume_classification( + test_id: str, + csubst: CSubst | None, + indeterminate: bool | None, + expected: type[SubsumptionCheck], +) -> None: + # Given a prover whose implies returns a CTermImplies with the given csubst / indeterminate + prover = Mock() + prover.fast_check_subsumption = False + prover.assume_defined = False + prover.kcfg_explore.cterm_symbolic.implies.return_value = CTermImplies(csubst, (), None, (), indeterminate) + + # When (call the unbound method with the Mock as self) + result = APRProver._check_subsume(prover, Mock(id=1), Mock(id=2), proof_id='p') + + # Then the verdict is classified per §1c + assert isinstance(result, expected) + if isinstance(result, Subsumed): + assert result.csubst is csubst + + +def test_check_subsume_fast_skip_is_decisive_invalid() -> None: + # Given the fast may-subsume heuristic rejects subsumption + prover = Mock() + prover.fast_check_subsumption = True + prover._may_subsume.return_value = False + + # When + result = APRProver._check_subsume(prover, Mock(id=1), Mock(id=2), proof_id='p') + + # Then it is a decisive non-subsumption and the backend is never consulted + assert isinstance(result, DecisiveInvalid) + prover.kcfg_explore.cterm_symbolic.implies.assert_not_called() + + def test_apr_proof_minimization_and_terminals() -> None: # 25 /-- X >=Int 5 --> 10 # 5 10 15 20 /-- X >=Int 0 --> 6 --> 8 From 2e9bd0c6a60a4fa7310e17fe6d48c5bce3b15e99 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 30 May 2026 18:13:09 +0000 Subject: [PATCH 07/26] kcfg/{kcfg,store}, tests/unit/test_kcfg: add Node.variants (Producer, NodeVariant) and public add_variant MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 (cherry picked from commit ed95720fd8ac1f6f766c9a72ac243c82758f755b) --- pyk/src/pyk/kcfg/kcfg.py | 102 +++++++++++++++++++++++++++++--- pyk/src/pyk/kcfg/store.py | 16 +++-- pyk/src/tests/unit/test_kcfg.py | 69 +++++++++++++++++++++ 3 files changed, 173 insertions(+), 14 deletions(-) diff --git a/pyk/src/pyk/kcfg/kcfg.py b/pyk/src/pyk/kcfg/kcfg.py index 20268b2376..9e28188d3e 100644 --- a/pyk/src/pyk/kcfg/kcfg.py +++ b/pyk/src/pyk/kcfg/kcfg.py @@ -5,6 +5,7 @@ from abc import ABC, abstractmethod from collections.abc import Container from dataclasses import dataclass, field +from enum import Enum from threading import RLock from typing import TYPE_CHECKING, Final, List, Union, cast, final @@ -51,6 +52,39 @@ class KCFGNodeAttr(NodeAttr): STUCK = NodeAttr('stuck') +class Producer(Enum): + """How a node's term was produced — the basis for a node's recover-mode 'rung'. + + ``INIT`` is the original term; ``BOOSTER_SIMPLIFY`` / ``KORE_SIMPLIFY`` record a + re-simplification that produced a new term (booster-only, then kore-enabled). + """ + + INIT = 'init' + BOOSTER_SIMPLIFY = 'simplified-booster' + KORE_SIMPLIFY = 'simplified-booster-kore' + + +@final +@dataclass(frozen=True) +class NodeVariant: + """One entry in a node's simplification-provenance chain (`KCFG.Node.variants`). + + Records the term produced by a simplification step and the producer + JSON-RPC ``request_id`` + that produced it. The chain is flat (least→most simplified) with the canonical term last. + """ + + producer: Producer + request_id: str | None # the simplify RPC that produced this cterm; None for INIT + cterm: CTerm + + def to_dict(self) -> dict[str, Any]: + return {'producer': self.producer.value, 'request_id': self.request_id, 'cterm': self.cterm.to_dict()} + + @staticmethod + def from_dict(dct: dict[str, Any]) -> NodeVariant: + return NodeVariant(Producer(dct['producer']), dct.get('request_id'), CTerm.from_dict(dct['cterm'])) + + class KCFGStore: store_path: Path @@ -117,34 +151,61 @@ class Node: id: int cterm: CTerm attrs: frozenset[NodeAttr] - - def __init__(self, id: int, cterm: CTerm, attrs: Iterable[NodeAttr] = ()) -> None: + # Simplification-provenance chain, least→most simplified, canonical term last; `()` == no + # recorded history (back-compat default). `compare=False` excludes it from the dataclass's + # generated eq/order/hash, so node identity is unchanged — `cterm` already reflects the + # canonical term, and the rest of the system stays oblivious to `variants` (see C8). + variants: tuple[NodeVariant, ...] = field(default=(), compare=False) + + def __init__( + self, id: int, cterm: CTerm, attrs: Iterable[NodeAttr] = (), variants: Iterable[NodeVariant] = () + ) -> None: object.__setattr__(self, 'id', id) object.__setattr__(self, 'cterm', cterm) object.__setattr__(self, 'attrs', frozenset(attrs)) + object.__setattr__(self, 'variants', tuple(variants)) def to_dict(self) -> dict[str, Any]: - return {'id': self.id, 'cterm': self.cterm.to_dict(), 'attrs': [attr.value for attr in self.attrs]} + dct: dict[str, Any] = { + 'id': self.id, + 'cterm': self.cterm.to_dict(), + 'attrs': [attr.value for attr in self.attrs], + } + # Omitted when empty so variant-less nodes serialise byte-identically to before. + if self.variants: + dct['variants'] = [variant.to_dict() for variant in self.variants] + return dct @staticmethod def from_dict(dct: dict[str, Any]) -> KCFG.Node: - return KCFG.Node(dct['id'], CTerm.from_dict(dct['cterm']), [NodeAttr(attr) for attr in dct['attrs']]) + return KCFG.Node( + dct['id'], + CTerm.from_dict(dct['cterm']), + [NodeAttr(attr) for attr in dct['attrs']], + [NodeVariant.from_dict(v) for v in dct.get('variants', ())], + ) def add_attr(self, attr: NodeAttr) -> KCFG.Node: - return KCFG.Node(self.id, self.cterm, list(self.attrs) + [attr]) + return KCFG.Node(self.id, self.cterm, list(self.attrs) + [attr], self.variants) def remove_attr(self, attr: NodeAttr) -> KCFG.Node: if attr not in self.attrs: raise ValueError(f'Node {self.id} does not have attribute {attr.value}') - return KCFG.Node(self.id, self.cterm, self.attrs.difference([attr])) + return KCFG.Node(self.id, self.cterm, self.attrs.difference([attr]), self.variants) def discard_attr(self, attr: NodeAttr) -> KCFG.Node: - return KCFG.Node(self.id, self.cterm, self.attrs.difference([attr])) + return KCFG.Node(self.id, self.cterm, self.attrs.difference([attr]), self.variants) - def let(self, cterm: CTerm | None = None, attrs: Iterable[KCFGNodeAttr] | None = None) -> KCFG.Node: + def let( + self, + cterm: CTerm | None = None, + attrs: Iterable[KCFGNodeAttr] | None = None, + variants: Iterable[NodeVariant] | None = None, + ) -> KCFG.Node: new_cterm = cterm if cterm is not None else self.cterm new_attrs = attrs if attrs is not None else self.attrs - return KCFG.Node(self.id, new_cterm, new_attrs) + new_variants = variants if variants is not None else self.variants + return KCFG.Node(self.id, new_cterm, new_attrs, new_variants) @property def free_vars(self) -> frozenset[str]: @@ -856,6 +917,29 @@ def let_node( new_node = node.let(cterm=cterm, attrs=attrs) self.replace_node(new_node) + def add_variant( + self, + node_id: NodeIdLike, + producer: Producer, + cterm: CTerm, + request_id: str | None = None, + ) -> KCFG.Node: + """Append a simplification variant to a node and make its term canonical. + + Non-destructive provenance: the node's ``cterm`` is updated to the most-simplified term + (so downstream readers see it transparently) while ``variants`` records the full chain. + On the first variant the original term is seeded as an ``INIT`` entry, so the chain is + self-contained (``variants[i-1].cterm`` → ``variants[i].cterm`` is always a real step). + + Exposed publicly so downstream (e.g. kevm-pyk init/target pre-simplification) can drive it. + """ + node = self.node(node_id) + chain = node.variants if node.variants else (NodeVariant(Producer.INIT, None, node.cterm),) + new_variants = chain + (NodeVariant(producer, request_id, cterm),) + new_node = node.let(cterm=cterm, variants=new_variants) + self.replace_node(new_node) + return new_node + def replace_node(self, node: KCFG.Node) -> None: self._nodes[node.id] = node self._created_nodes.add(node.id) diff --git a/pyk/src/pyk/kcfg/store.py b/pyk/src/pyk/kcfg/store.py index 0488bf3778..5661e3ffbd 100644 --- a/pyk/src/pyk/kcfg/store.py +++ b/pyk/src/pyk/kcfg/store.py @@ -8,7 +8,7 @@ from ..cterm import CTerm from ..kast.inner import KApply, KSequence, KToken, KVariable, bottom_up_with_summary -from .kcfg import KCFG +from .kcfg import KCFG, NodeVariant if TYPE_CHECKING: from collections.abc import Iterator @@ -39,12 +39,18 @@ def __getitem__(self, key: int) -> KCFG.Node: return self._nodes[key] def __setitem__(self, key: int, node: KCFG.Node) -> None: - old_cterm = node.cterm - new_config = self._optimize(old_cterm.config) - new_constraints = tuple(self._optimize(c) for c in old_cterm.constraints) - new_node = KCFG.Node(node.id, CTerm(new_config, new_constraints), attrs=node.attrs) + # Term-dedup the canonical cterm and every variant cterm, carrying the provenance chain + # through unchanged (variants must survive the store, see C8). + new_variants = tuple( + NodeVariant(variant.producer, variant.request_id, self._optimize_cterm(variant.cterm)) + for variant in node.variants + ) + new_node = KCFG.Node(node.id, self._optimize_cterm(node.cterm), attrs=node.attrs, variants=new_variants) self._nodes[key] = new_node + def _optimize_cterm(self, cterm: CTerm) -> CTerm: + return CTerm(self._optimize(cterm.config), tuple(self._optimize(c) for c in cterm.constraints)) + def __delitem__(self, key: int) -> None: del self._nodes[key] diff --git a/pyk/src/tests/unit/test_kcfg.py b/pyk/src/tests/unit/test_kcfg.py index f9dc69d1b0..40027be89f 100644 --- a/pyk/src/tests/unit/test_kcfg.py +++ b/pyk/src/tests/unit/test_kcfg.py @@ -252,6 +252,75 @@ def test_create_node() -> None: assert not cfg.is_stuck(new_node.id) +def test_node_variants_default_empty_and_roundtrip() -> None: + # Given a node built the legacy way + n = node(1) + + # Then variants default to empty and the serialised form omits the key + assert n.variants == () + assert 'variants' not in n.to_dict() + # And a legacy node dict (no 'variants') still loads + assert KCFG.Node.from_dict(n.to_dict()) == n + + +def test_add_variant_chains_and_updates_cterm() -> None: + from pyk.kcfg.kcfg import Producer + + # Given a fresh node at rung 0 + cfg = KCFG() + n = cfg.create_node(term(1)) + + # When a booster-simplify variant is appended + cfg.add_variant(n.id, Producer.BOOSTER_SIMPLIFY, term(2), request_id='claim-001') + updated = cfg.node(n.id) + + # Then the canonical cterm advances and the chain seeds INIT then records the step + assert updated.cterm == term(2) + assert [v.producer for v in updated.variants] == [Producer.INIT, Producer.BOOSTER_SIMPLIFY] + assert updated.variants[0].cterm == term(1) + assert updated.variants[-1].cterm == term(2) + assert updated.variants[-1].request_id == 'claim-001' + + # When a second (kore-simplify) variant is appended, INIT is not re-seeded + cfg.add_variant(n.id, Producer.KORE_SIMPLIFY, term(3), request_id='claim-002') + updated = cfg.node(n.id) + assert updated.cterm == term(3) + assert [v.producer for v in updated.variants] == [ + Producer.INIT, + Producer.BOOSTER_SIMPLIFY, + Producer.KORE_SIMPLIFY, + ] + + +def test_node_variants_to_dict_from_dict_roundtrip() -> None: + from pyk.kcfg.kcfg import Producer + + # Given a node carrying a variant chain + cfg = KCFG() + n = cfg.create_node(term(1)) + cfg.add_variant(n.id, Producer.BOOSTER_SIMPLIFY, term(2), request_id='r-1') + original = cfg.node(n.id) + + # When round-tripped through dict + restored = KCFG.Node.from_dict(original.to_dict()) + + # Then variants survive (equality ignores variants, so compare them explicitly) + assert restored == original + assert restored.variants == original.variants + + +def test_node_equality_ignores_variants() -> None: + from pyk.kcfg.kcfg import NodeVariant, Producer + + # Given two nodes identical but for their variant chains + bare = KCFG.Node(1, term(1)) + with_variants = KCFG.Node(1, term(1), variants=[NodeVariant(Producer.INIT, None, term(1))]) + + # Then they compare equal and hash equal (variants is metadata) + assert bare == with_variants + assert hash(bare) == hash(with_variants) + + def test_remove_unknown_node() -> None: # Given cfg = KCFG() From 4a2653aeb81399915588f33a055d654e9795ae57 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 30 May 2026 18:15:46 +0000 Subject: [PATCH 08/26] kcfg/kcfg, tests/unit/test_kcfg: add recover-mode node attrs and KoreHandoff / 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 (cherry picked from commit d0e4b68045260256906e5d95d81a24ef9292c407) --- pyk/src/pyk/kcfg/kcfg.py | 43 +++++++++++++++++++++++++++++++++ pyk/src/tests/unit/test_kcfg.py | 38 +++++++++++++++++++++++++++++ 2 files changed, 81 insertions(+) diff --git a/pyk/src/pyk/kcfg/kcfg.py b/pyk/src/pyk/kcfg/kcfg.py index 9e28188d3e..a704a0817e 100644 --- a/pyk/src/pyk/kcfg/kcfg.py +++ b/pyk/src/pyk/kcfg/kcfg.py @@ -50,6 +50,11 @@ class NodeAttr: class KCFGNodeAttr(NodeAttr): VACUOUS = NodeAttr('vacuous') STUCK = NodeAttr('stuck') + # Recover-mode bookkeeping (inert outside recover-mode): + BOOSTER_TRIED = NodeAttr('booster-tried') # a booster `try` made no progress on the current term + KORE_TRIED = NodeAttr('kore-tried') # a kore `try` made no progress on the current term + SUBSUME_INDETERMINATE = NodeAttr('subsume-indeterminate') # last booster subsumption was indeterminate + BOTH_BACKENDS_FAILED = NodeAttr('both-backends-failed') # terminal: neither backend could advance the node class Producer(Enum): @@ -85,6 +90,29 @@ def from_dict(dct: dict[str, Any]) -> NodeVariant: return NodeVariant(Producer(dct['producer']), dct.get('request_id'), CTerm.from_dict(dct['cterm'])) +@final +@dataclass(frozen=True) +class KoreHandoff: + """Record an operation-level kore handoff (execute or implies) where kore advanced the proof. + + Lets the diagnostic find every kore handoff without scanning logs. ``request_id`` is the join + key onto the stored per-request log (Layer 5). For ``execute``, ``source``/``target`` are the + lhs/rhs node ids; for ``implies``, ``source`` is the node and ``target`` the subsumption target. + """ + + source: int + target: int + flavour: str # 'execute' | 'implies' + request_id: str + + def to_dict(self) -> dict[str, Any]: + return {'source': self.source, 'target': self.target, 'flavour': self.flavour, 'request_id': self.request_id} + + @staticmethod + def from_dict(dct: dict[str, Any]) -> KoreHandoff: + return KoreHandoff(dct['source'], dct['target'], dct['flavour'], dct['request_id']) + + class KCFGStore: store_path: Path @@ -500,6 +528,8 @@ def replace_target(self, node: KCFG.Node) -> KCFG.NDBranch: _aliases: dict[str, int] _lock: RLock + _kore_handoffs: list[KoreHandoff] + _kcfg_store: KCFGStore | None def __init__(self, cfg_dir: Path | None = None, optimize_memory: bool = True) -> None: @@ -519,6 +549,7 @@ def __init__(self, cfg_dir: Path | None = None, optimize_memory: bool = True) -> self._ndbranches = {} self._aliases = {} self._lock = RLock() + self._kore_handoffs = [] if cfg_dir is not None: self._kcfg_store = KCFGStore(cfg_dir) @@ -699,6 +730,7 @@ def to_dict_no_nodes(self) -> dict[str, Any]: 'splits': splits, 'ndbranches': ndbranches, 'aliases': aliases, + 'kore_handoffs': [handoff.to_dict() for handoff in self._kore_handoffs], } return {k: v for k, v in res.items() if v} @@ -721,6 +753,7 @@ def to_dict(self) -> dict[str, Any]: 'splits': splits, 'ndbranches': ndbranches, 'aliases': aliases, + 'kore_handoffs': [handoff.to_dict() for handoff in self._kore_handoffs], } return {k: v for k, v in res.items() if v} @@ -758,6 +791,9 @@ def from_dict(dct: Mapping[str, Any], optimize_memory: bool = True) -> KCFG: for alias, node_id in dct.get('aliases', {}).items(): cfg.add_alias(alias=alias, node_id=node_id) + for handoff_dict in dct.get('kore_handoffs') or []: + cfg.add_kore_handoff(KoreHandoff.from_dict(handoff_dict)) + return cfg def aliases(self, node_id: NodeIdLike) -> list[str]: @@ -940,6 +976,13 @@ def add_variant( self.replace_node(new_node) return new_node + @property + def kore_handoffs(self) -> list[KoreHandoff]: + return list(self._kore_handoffs) + + def add_kore_handoff(self, handoff: KoreHandoff) -> None: + self._kore_handoffs.append(handoff) + def replace_node(self, node: KCFG.Node) -> None: self._nodes[node.id] = node self._created_nodes.add(node.id) diff --git a/pyk/src/tests/unit/test_kcfg.py b/pyk/src/tests/unit/test_kcfg.py index 40027be89f..2a044cd648 100644 --- a/pyk/src/tests/unit/test_kcfg.py +++ b/pyk/src/tests/unit/test_kcfg.py @@ -321,6 +321,44 @@ def test_node_equality_ignores_variants() -> None: assert hash(bare) == hash(with_variants) +def test_kore_handoffs_add_and_roundtrip() -> None: + from pyk.kcfg.kcfg import KoreHandoff + + # Given a kcfg with two recorded handoffs + cfg = KCFG() + cfg.create_node(term(1)) + cfg.add_kore_handoff(KoreHandoff(source=1, target=2, flavour='execute', request_id='claim-003')) + cfg.add_kore_handoff(KoreHandoff(source=2, target=2, flavour='implies', request_id='claim-004')) + + # Then the accessor returns them and they round-trip through to_dict/from_dict + assert len(cfg.kore_handoffs) == 2 + restored = KCFG.from_dict(cfg.to_dict()) + assert restored.kore_handoffs == cfg.kore_handoffs + + +def test_kore_handoffs_omitted_when_empty() -> None: + # Given a kcfg with no handoffs + cfg = KCFG() + cfg.create_node(term(1)) + + # Then the key is omitted from both serialisations (additive / back-compat) + assert 'kore_handoffs' not in cfg.to_dict() + assert 'kore_handoffs' not in cfg.to_dict_no_nodes() + + +def test_recover_mode_node_attrs_serialise() -> None: + # Given a node carrying the new recover-mode attrs + cfg = KCFG() + n = cfg.create_node(term(1)) + cfg.add_attr(n.id, KCFGNodeAttr.BOOSTER_TRIED) + cfg.add_attr(n.id, KCFGNodeAttr.SUBSUME_INDETERMINATE) + + # Then the attrs round-trip through the in-memory Node serialisation + restored = KCFG.Node.from_dict(cfg.node(n.id).to_dict()) + assert KCFGNodeAttr.BOOSTER_TRIED in restored.attrs + assert KCFGNodeAttr.SUBSUME_INDETERMINATE in restored.attrs + + def test_remove_unknown_node() -> None: # Given cfg = KCFG() From 32af8659c6025f35018725b1a17f1142866860c5 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 30 May 2026 18:19:08 +0000 Subject: [PATCH 09/26] kcfg/kcfg, tests/unit/kcfg/test_store: persist new attrs and variants 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 (cherry picked from commit 4454551e39791caba3eed9e514e3fcf10e9f29df) --- pyk/src/pyk/kcfg/kcfg.py | 41 ++++++++++++-------- pyk/src/tests/unit/kcfg/test_store.py | 56 ++++++++++++++++++++++++++- 2 files changed, 80 insertions(+), 17 deletions(-) diff --git a/pyk/src/pyk/kcfg/kcfg.py b/pyk/src/pyk/kcfg/kcfg.py index a704a0817e..4a828ef002 100644 --- a/pyk/src/pyk/kcfg/kcfg.py +++ b/pyk/src/pyk/kcfg/kcfg.py @@ -116,6 +116,18 @@ def from_dict(dct: dict[str, Any]) -> KoreHandoff: class KCFGStore: store_path: Path + # Node attributes persisted as top-level side-lists in `kcfg.json` (node files only carry + # `cterm`/`variants`; `read_cfg_data` rebuilds `attrs` from these). Keep this the single source + # of truth so adding a persisted attr is a one-line change (see C10). + _ATTR_SIDE_LISTS: Final = { + 'vacuous': KCFGNodeAttr.VACUOUS, + 'stuck': KCFGNodeAttr.STUCK, + 'booster_tried': KCFGNodeAttr.BOOSTER_TRIED, + 'kore_tried': KCFGNodeAttr.KORE_TRIED, + 'subsume_indeterminate': KCFGNodeAttr.SUBSUME_INDETERMINATE, + 'both_backends_failed': KCFGNodeAttr.BOTH_BACKENDS_FAILED, + } + def __init__(self, store_path: Path) -> None: self.store_path = store_path ensure_dir_path(store_path) @@ -135,12 +147,8 @@ def kcfg_node_path(self, node_id: int) -> Path: def write_cfg_data( self, kcfg: KCFG, dct: dict[str, Any], deleted_nodes: Iterable[int] = (), created_nodes: Iterable[int] = () ) -> None: - vacuous_nodes = [ - node_id for node_id in kcfg._nodes.keys() if KCFGNodeAttr.VACUOUS in kcfg._nodes[node_id].attrs - ] - stuck_nodes = [node_id for node_id in kcfg._nodes.keys() if KCFGNodeAttr.STUCK in kcfg._nodes[node_id].attrs] - dct['vacuous'] = vacuous_nodes - dct['stuck'] = stuck_nodes + for key, attr in self._ATTR_SIDE_LISTS.items(): + dct[key] = [node_id for node_id in kcfg._nodes.keys() if attr in kcfg._nodes[node_id].attrs] for node_id in deleted_nodes: self.kcfg_node_path(node_id).unlink(missing_ok=True) for node_id in created_nodes: @@ -150,21 +158,22 @@ def write_cfg_data( def read_cfg_data(self) -> dict[str, Any]: dct = json.loads(self.kcfg_json_path.read_text()) nodes = [self.read_node_data(node_id) for node_id in dct.get('nodes') or []] - dct['nodes'] = nodes new_nodes = [] - for node in dct['nodes']: - attrs = [] - if node['id'] in dct['vacuous']: - attrs.append(KCFGNodeAttr.VACUOUS.value) - if node['id'] in dct['stuck']: - attrs.append(KCFGNodeAttr.STUCK.value) - new_nodes.append({'id': node['id'], 'cterm': node['cterm'], 'attrs': attrs}) + for node in nodes: + # Rebuild attrs from the side-lists; carry `variants` through from the node file + # (`KCFG.Node.from_dict` ignores it if absent). `dct.get` keeps old stores (which lack + # the new keys) loadable. + attrs = [attr.value for key, attr in self._ATTR_SIDE_LISTS.items() if node['id'] in (dct.get(key) or [])] + new_node: dict[str, Any] = {'id': node['id'], 'cterm': node['cterm'], 'attrs': attrs} + if 'variants' in node: + new_node['variants'] = node['variants'] + new_nodes.append(new_node) dct['nodes'] = new_nodes - del dct['vacuous'] - del dct['stuck'] + for key in self._ATTR_SIDE_LISTS: + dct.pop(key, None) return dct diff --git a/pyk/src/tests/unit/kcfg/test_store.py b/pyk/src/tests/unit/kcfg/test_store.py index 68f31f782c..a4e8992973 100644 --- a/pyk/src/tests/unit/kcfg/test_store.py +++ b/pyk/src/tests/unit/kcfg/test_store.py @@ -1,5 +1,6 @@ from __future__ import annotations +import json from itertools import count from typing import TYPE_CHECKING @@ -8,12 +9,13 @@ from pyk.cterm import CTerm from pyk.kast.inner import KApply, KSequence from pyk.kast.prelude.utils import token -from pyk.kcfg.kcfg import KCFG +from pyk.kcfg.kcfg import KCFG, KCFGNodeAttr, KoreHandoff, Producer from pyk.kcfg.store import OptimizedNodeStore, _Cache from ..utils import a, b, c, f if TYPE_CHECKING: + from pathlib import Path from typing import Final from pyk.kast import KInner @@ -81,3 +83,55 @@ def test_optimized_store() -> None: for idx, item in zip(range(0, len(OPTIMIZE_TEST_DATA)), OPTIMIZE_TEST_DATA, strict=True): assert KCFG.Node(idx, CTerm(KApply('', item), ())) == store[idx] + + +def _cell(i: int) -> CTerm: + return CTerm(KApply('', token(i))) + + +def test_kcfg_store_roundtrip_preserves_attrs_variants_handoffs(tmp_path: Path) -> None: + # Given a kcfg (on disk) carrying new attrs, a variant chain, and a handoff + cfg = KCFG(tmp_path / 'kcfg') + n1 = cfg.create_node(_cell(1)) + n2 = cfg.create_node(_cell(2)) + cfg.add_attr(n1.id, KCFGNodeAttr.BOOSTER_TRIED) + cfg.add_attr(n1.id, KCFGNodeAttr.SUBSUME_INDETERMINATE) + cfg.add_attr(n2.id, KCFGNodeAttr.STUCK) + cfg.add_attr(n2.id, KCFGNodeAttr.BOTH_BACKENDS_FAILED) + cfg.add_variant(n1.id, Producer.BOOSTER_SIMPLIFY, _cell(3), request_id='r-1') + cfg.add_kore_handoff(KoreHandoff(source=n1.id, target=n2.id, flavour='execute', request_id='r-2')) + + # When written and read back through KCFGStore + cfg.write_cfg_data() + restored = KCFG.read_cfg_data(tmp_path / 'kcfg') + + # Then attrs, the variant chain (and canonical cterm), and handoffs all survive + rn1 = restored.node(n1.id) + assert KCFGNodeAttr.BOOSTER_TRIED in rn1.attrs + assert KCFGNodeAttr.SUBSUME_INDETERMINATE in rn1.attrs + assert rn1.cterm == _cell(3) + assert [v.producer for v in rn1.variants] == [Producer.INIT, Producer.BOOSTER_SIMPLIFY] + rn2 = restored.node(n2.id) + assert KCFGNodeAttr.STUCK in rn2.attrs + assert KCFGNodeAttr.BOTH_BACKENDS_FAILED in rn2.attrs + assert restored.kore_handoffs == [KoreHandoff(source=n1.id, target=n2.id, flavour='execute', request_id='r-2')] + + +def test_kcfg_store_loads_legacy_without_new_keys(tmp_path: Path) -> None: + # Given a store written, then downgraded to look like an old one (new side-list keys removed) + cfg = KCFG(tmp_path / 'kcfg') + n = cfg.create_node(_cell(1)) + cfg.add_attr(n.id, KCFGNodeAttr.STUCK) + cfg.write_cfg_data() + + kcfg_json = tmp_path / 'kcfg' / 'kcfg.json' + dct = json.loads(kcfg_json.read_text()) + for key in ['booster_tried', 'kore_tried', 'subsume_indeterminate', 'both_backends_failed', 'kore_handoffs']: + dct.pop(key, None) + kcfg_json.write_text(json.dumps(dct)) + + # When read back, the legacy store still loads and the pre-existing attr survives + restored = KCFG.read_cfg_data(tmp_path / 'kcfg') + assert restored.node(n.id).cterm == _cell(1) + assert KCFGNodeAttr.STUCK in restored.node(n.id).attrs + assert restored.kore_handoffs == [] From 03674fb08570271e6c11abb1c6310897192e6193 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 30 May 2026 18:33:00 +0000 Subject: [PATCH 10/26] kore/rpc, cterm/symbolic, kcfg/explore, tests/unit/kcfg/test_explore: variant-appending simplify helper with request_id + log-entry capture MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 (cherry picked from commit 3eaa3e3cd05d513e29766dbf8305b1a3ab195f96) --- pyk/src/pyk/cterm/symbolic.py | 11 +++++- pyk/src/pyk/kcfg/explore.py | 39 ++++++++++++++++++-- pyk/src/pyk/kore/rpc.py | 22 ++++++++++-- pyk/src/tests/unit/kcfg/test_explore.py | 48 ++++++++++++++++++++++++- 4 files changed, 113 insertions(+), 7 deletions(-) diff --git a/pyk/src/pyk/cterm/symbolic.py b/pyk/src/pyk/cterm/symbolic.py index abbcadd0fa..bf2b82d4b8 100644 --- a/pyk/src/pyk/cterm/symbolic.py +++ b/pyk/src/pyk/cterm/symbolic.py @@ -155,6 +155,16 @@ def _capture_haskell_log(self, entries: tuple[Any, ...] | None) -> None: log_file = self._haskell_log_dir / f'{request_id}.jsonl' log_file.write_text('\n'.join(json.dumps(entry) for entry in entries) + '\n') + @property + def last_request_id(self) -> str | None: + """JSON-RPC id of the most recent RPC issued on this thread (see `KoreClient.last_request_id`).""" + return self._kore_client.last_request_id + + @property + def last_haskell_log_entries(self) -> tuple[Any, ...] | None: + """`haskell-log-entries` bundle of the most recent RPC on this thread (see `KoreClient`).""" + return self._kore_client.last_haskell_log_entries + def execute( self, cterm: CTerm, @@ -165,7 +175,6 @@ def execute( booster_only_simplify: bool | None = None, haskell_logging: bool | None = None, raise_on_aborted: bool = True, - haskell_logging: bool | None = None, ) -> CTermExecute: _LOGGER.debug(f'Executing: {cterm}') diff --git a/pyk/src/pyk/kcfg/explore.py b/pyk/src/pyk/kcfg/explore.py index 07704f57fb..141c7b0f0e 100644 --- a/pyk/src/pyk/kcfg/explore.py +++ b/pyk/src/pyk/kcfg/explore.py @@ -2,7 +2,7 @@ import logging from functools import cached_property -from typing import TYPE_CHECKING +from typing import TYPE_CHECKING, NamedTuple from ..kast.inner import KApply, KVariable from ..kast.manip import ( @@ -17,12 +17,12 @@ from ..kast.pretty import PrettyPrinter from ..kore.rpc import LogRewrite, RewriteSuccess from ..utils import not_none, shorten_hashes, single, unique -from .kcfg import KCFG, Abstract, Branch, NDBranch, NoProgress, Step, Vacuous +from .kcfg import KCFG, Abstract, Branch, NDBranch, NoProgress, Producer, Step, Vacuous from .semantics import DefaultSemantics if TYPE_CHECKING: from collections.abc import Iterable - from typing import Final + from typing import Any, Final from ..cterm import CTerm, CTermSymbolic from ..kast import KInner @@ -35,6 +35,20 @@ _LOGGER: Final = logging.getLogger(__name__) +class SimplifyVariant(NamedTuple): + """Result of a recover-mode variant-producing simplification. + + Carries everything the coordinator needs to land the variant (`KCFG.add_variant`) and store its + captured logs (keyed by `request_id`): the `producer`, the simplified `cterm`, the simplify RPC's + `request_id`, and the `haskell-log-entries` bundle (`None` if the backend captured nothing). + """ + + producer: Producer + cterm: CTerm + request_id: str | None + log_entries: tuple[Any, ...] | None + + class KCFGExplore: cterm_symbolic: CTermSymbolic @@ -136,6 +150,25 @@ def simplify(self, cfg: KCFG, logs: dict[int, tuple[LogEntry, ...]]) -> None: else: logs[node.id] = next_node_logs + def simplify_variant(self, cterm: CTerm, *, booster_only: bool) -> SimplifyVariant: + """Re-simplify ``cterm`` with one backend, capturing the request id and per-request logs. + + Non-destructive: returns a `SimplifyVariant` for the coordinator to land via + `KCFG.add_variant`; the recover-mode ladder uses `booster_only=True` (rung 0→1) then + `booster_only=False` (rung 1→2). Always logs (`haskell_logging=True`) — every simplify on + the ladder is diagnostic-relevant. + """ + producer = Producer.BOOSTER_SIMPLIFY if booster_only else Producer.KORE_SIMPLIFY + simplified, _logs = self.cterm_symbolic.simplify( + cterm, booster_only_simplify=booster_only, haskell_logging=True + ) + return SimplifyVariant( + producer=producer, + cterm=simplified, + request_id=self.cterm_symbolic.last_request_id, + log_entries=self.cterm_symbolic.last_haskell_log_entries, + ) + def step( self, cfg: KCFG, diff --git a/pyk/src/pyk/kore/rpc.py b/pyk/src/pyk/kore/rpc.py index 14eb642189..4b7aba0bee 100644 --- a/pyk/src/pyk/kore/rpc.py +++ b/pyk/src/pyk/kore/rpc.py @@ -14,7 +14,7 @@ from pathlib import Path from signal import SIGINT from subprocess import DEVNULL, PIPE, Popen -from threading import Thread +from threading import Thread, local from time import sleep from typing import ClassVar # noqa: TC003 from typing import TYPE_CHECKING, ContextManager, NamedTuple, TypedDict, final @@ -48,6 +48,11 @@ # `ContextVar` values are not propagated by `ThreadPoolExecutor`. client_label: ContextVar[str | None] = ContextVar('kore_rpc_client_label', default=None) +# Records the `haskell-log-entries` bundle (or None) of the most recent response on the calling +# thread. Snapshotted alongside `last_request_id` so a diagnostic worker can capture the per-request +# logs of the exact call it just made without threading them through every result type. +_last_haskell_log_entries: local = local() + class KoreExecLogFormat(Enum): STANDARD = 'standard' @@ -1019,11 +1024,24 @@ def last_request_id(self) -> str | None: """ return self._client.last_request_id + @property + def last_haskell_log_entries(self) -> tuple[Any, ...] | None: + """The ``haskell-log-entries`` bundle of the most recent response on the calling thread. + + ``None`` when the last request did not set ``haskell-logging`` (or before any request). + Snapshot alongside ``last_request_id`` to store the per-request logs of that exact call. + """ + return getattr(_last_haskell_log_entries, 'value', None) + def _request(self, method: str, **params: Any) -> dict[str, Any]: try: - return self._client.request(method, **params) + result = self._client.request(method, **params) except JsonRpcError as err: raise self._error(err) from err + # Capture the per-request log bundle (if any) on this thread for `last_haskell_log_entries`. + entries = result.get('haskell-log-entries') + _last_haskell_log_entries.value = tuple(entries) if entries is not None else None + return result def _error(self, err: JsonRpcError) -> KoreClientError: assert err.code not in {-32601, -32602}, 'Malformed Kore-RPC request' diff --git a/pyk/src/tests/unit/kcfg/test_explore.py b/pyk/src/tests/unit/kcfg/test_explore.py index b3dd9e8cc7..64ca01b06c 100644 --- a/pyk/src/tests/unit/kcfg/test_explore.py +++ b/pyk/src/tests/unit/kcfg/test_explore.py @@ -2,9 +2,11 @@ from unittest.mock import Mock +import pytest + from pyk.cterm.symbolic import CTermExecute from pyk.kcfg.explore import KCFGExplore -from pyk.kcfg.kcfg import NoProgress, Step +from pyk.kcfg.kcfg import NoProgress, Producer, Step from ..test_kcfg import term @@ -41,3 +43,47 @@ def test_extend_cterm_step_on_progress() -> None: # Then a basic-block Step is produced (unchanged behaviour) assert len(results) == 1 assert isinstance(results[0], Step) + + +@pytest.mark.parametrize( + 'booster_only,expected_producer', + [(True, Producer.BOOSTER_SIMPLIFY), (False, Producer.KORE_SIMPLIFY)], + ids=['booster', 'kore'], +) +def test_simplify_variant_producer_and_capture(booster_only: bool, expected_producer: Producer) -> None: + # Given a cterm_symbolic that simplifies to a new term and exposes request id + log entries + entries = ({'context': ['proxy'], 'message': 'x'},) + cterm_symbolic = Mock() + cterm_symbolic.simplify.return_value = (term(2), ()) + cterm_symbolic.last_request_id = 'claim-001' + cterm_symbolic.last_haskell_log_entries = entries + explore = KCFGExplore(cterm_symbolic) + + # When + variant = explore.simplify_variant(term(1), booster_only=booster_only) + + # Then the producer matches the backend, and request_id + entries are captured + assert variant.producer is expected_producer + assert variant.cterm == term(2) + assert variant.request_id == 'claim-001' + assert variant.log_entries == entries + # And the simplify was invoked with logging on and the right backend + _args, kwargs = cterm_symbolic.simplify.call_args + assert kwargs['booster_only_simplify'] is booster_only + assert kwargs['haskell_logging'] is True + + +def test_simplify_variant_noop_still_yields_variant() -> None: + # Given a no-op simplification (term unchanged) + cterm_symbolic = Mock() + cterm_symbolic.simplify.return_value = (term(1), ()) + cterm_symbolic.last_request_id = 'claim-002' + cterm_symbolic.last_haskell_log_entries = None + explore = KCFGExplore(cterm_symbolic) + + # When + variant = explore.simplify_variant(term(1), booster_only=True) + + # Then a variant is still produced, whose cterm equals the input (the no-op is recorded) + assert variant.cterm == term(1) + assert variant.producer is Producer.BOOSTER_SIMPLIFY From 179d5becf77ea37a70a108e337a9847fafc21de7 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 30 May 2026 18:38:52 +0000 Subject: [PATCH 11/26] proof/reachability, tests/unit/test_proof: recover_mode flag, recover_task on APRProofStep, task selection in get_steps MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 (cherry picked from commit e3bb6627cc508a2afd4b482bfd6b46ca4704dec9) --- pyk/src/pyk/proof/reachability.py | 66 ++++++++++++++++++++++++++++++- pyk/src/tests/unit/test_proof.py | 46 ++++++++++++++++++++- 2 files changed, 109 insertions(+), 3 deletions(-) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 7be092d001..5259f5fc1b 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -5,6 +5,7 @@ import re from abc import ABC from dataclasses import dataclass, field +from enum import Enum from typing import TYPE_CHECKING, final from ..cterm.cterm import remove_useless_constraints @@ -14,7 +15,7 @@ from ..kast.prelude.ml import mlAnd, mlTop from ..kcfg import KCFG, KCFGStore from ..kcfg.exploration import KCFGExploration -from ..kcfg.kcfg import NoProgress +from ..kcfg.kcfg import KCFGNodeAttr, NoProgress, Producer from ..kore.rpc import LogEntry, client_label from ..ktool.claim_index import ClaimIndex from ..utils import FrozenDict, ensure_dir_path, hash_str, shorten_hashes, single @@ -36,6 +37,45 @@ _LOGGER: Final = logging.getLogger(__name__) +class RecoverTask(Enum): + """The per-node task the recover-mode coordinator assigns to a worker (see §unifying model). + + `TRY_BOOSTER`/`TRY_KORE` are the combined subsume-then-execute step with one backend; + `SIMPLIFY_BOOSTER`/`SIMPLIFY_KORE` each produce one re-simplification variant. + """ + + TRY_BOOSTER = 'try-booster' + SIMPLIFY_BOOSTER = 'simplify-booster' + SIMPLIFY_KORE = 'simplify-kore' + TRY_KORE = 'try-kore' + + +def recovery_rung(node: KCFG.Node) -> int: + """Compute the node's recovery rung: 0 (original), 1 (booster-simplified), 2 (kore-simplified). + + Derived from the producer of the most-simplified variant; an empty chain is rung 0. + """ + if not node.variants: + return 0 + return {Producer.INIT: 0, Producer.BOOSTER_SIMPLIFY: 1, Producer.KORE_SIMPLIFY: 2}[node.variants[-1].producer] + + +def recover_task_for(node: KCFG.Node) -> RecoverTask: + """Pick the next recover-mode task for a *pending* node from its rung and attrs (§3d). + + A pending node never has both `BOOSTER_TRIED` and `KORE_TRIED` at rung 2 — `commit` would have + marked that node stuck — so the rung-2 branch is always `TRY_KORE`. + """ + if KCFGNodeAttr.BOOSTER_TRIED not in node.attrs: + return RecoverTask.TRY_BOOSTER + rung = recovery_rung(node) + if rung == 0: + return RecoverTask.SIMPLIFY_BOOSTER + if rung == 1: + return RecoverTask.SIMPLIFY_KORE + return RecoverTask.TRY_KORE + + @dataclass class APRProofResult: node_id: int @@ -124,6 +164,7 @@ class APRProofStep: circularity: bool nonzero_depth: bool circularity_rule_id: str + recover_task: RecoverTask | None = None class APRProof(Proof[APRProofStep, APRProofResult], KCFGExploration): @@ -149,6 +190,9 @@ class APRProof(Proof[APRProofStep, APRProofResult], KCFGExploration): _exec_time: float error_info: Exception | None prior_loops_cache: dict[int, tuple[int, ...]] + # Runtime flag (not persisted): the prover sets it in `init_proof` so the coordinator's + # `get_steps`/`commit` run the recover-mode ladder. Resume re-supplies it via the CLI flag. + recover_mode: bool _checked_for_bounded: set[int] _next_steps: dict[NodeIdLike, KCFGExtendResult] @@ -192,6 +236,7 @@ def __init__( self._checked_for_bounded = set() self._next_steps = {} + self.recover_mode = False if self.proof_dir is not None and self.proof_subdir is not None: ensure_dir_path(self.proof_dir) @@ -233,12 +278,21 @@ def get_steps(self) -> list[APRProofStep]: single(predecessor_edges).source.id if predecessor_edges != [] else None ) + # Recover-mode: the coordinator picks the per-node task and disables extend-and-cache + # (caching a second extend interacts badly with re-trying a node across rungs, §3b). + recover_task = recover_task_for(node) if self.recover_mode else None + use_cache = ( + None + if self.recover_mode + else (predecessor_node_id if predecessor_node_id in self._next_steps else None) + ) + steps.append( APRProofStep( bmc_depth=self.bmc_depth, module_name=module_name, node=node, - use_cache=predecessor_node_id if predecessor_node_id in self._next_steps else None, + use_cache=use_cache, proof_id=self.id, target=self.kcfg.node(self.target), shortest_path_to_node=tuple(shortest_path), @@ -246,6 +300,7 @@ def get_steps(self) -> list[APRProofStep]: circularity=self.circularity, nonzero_depth=nonzero_depth, circularity_rule_id=f'{self.rule_id}-{self.init}-TO-{self.target}', + recover_task=recover_task, ) ) return steps @@ -765,6 +820,7 @@ class APRProver(Prover[APRProof, APRProofStep, APRProofResult]): kcfg_explore: KCFGExplore extra_module: KFlatModule | None optimize_kcfg: bool + recover_mode: bool def __init__( self, @@ -778,6 +834,7 @@ def __init__( assume_defined: bool = False, extra_module: KFlatModule | None = None, optimize_kcfg: bool = False, + recover_mode: bool = False, ) -> None: self.kcfg_explore = kcfg_explore @@ -791,6 +848,7 @@ def __init__( self.assume_defined = assume_defined self.extra_module = extra_module self.optimize_kcfg = optimize_kcfg + self.recover_mode = recover_mode def close(self) -> None: self.kcfg_explore.cterm_symbolic._kore_client.close() @@ -802,6 +860,10 @@ def init_proof(self, proof: APRProof) -> None: # their own closure — `ContextVar` is not propagated by ThreadPoolExecutor. client_label.set(proof.id) + # Propagate the prover's recover-mode config onto the proof so the coordinator's + # `get_steps`/`commit` (which live on the proof) run the recover-mode ladder. + proof.recover_mode = self.recover_mode + main_module_name = self.main_module_name if self.extra_module: main_module_name = self.kcfg_explore.cterm_symbolic.add_module(self.extra_module, name_as_id=True) diff --git a/pyk/src/tests/unit/test_proof.py b/pyk/src/tests/unit/test_proof.py index 50929f91d8..1fa2951958 100644 --- a/pyk/src/tests/unit/test_proof.py +++ b/pyk/src/tests/unit/test_proof.py @@ -10,7 +10,7 @@ from pyk.kast.prelude.kbool import BOOL from pyk.kast.prelude.kint import intToken from pyk.kcfg.exploration import KCFGExplorationNodeAttr -from pyk.kcfg.kcfg import KCFG, KCFGNodeAttr +from pyk.kcfg.kcfg import KCFG, KCFGNodeAttr, NodeVariant, Producer from pyk.proof import EqualityProof from pyk.proof.implies import EqualitySummary from pyk.proof.proof import CompositeSummary, Proof, ProofStatus @@ -22,7 +22,10 @@ APRSummary, DecisiveInvalid, Indeterminate, + RecoverTask, Subsumed, + recover_task_for, + recovery_rung, ) from .kcfg.test_minimize import minimization_test_kcfg @@ -34,6 +37,7 @@ from pytest import TempPathFactory + from pyk.kcfg.kcfg import NodeAttr from pyk.proof.reachability import SubsumptionCheck @@ -318,6 +322,46 @@ def test_check_subsume_fast_skip_is_decisive_invalid() -> None: prover.kcfg_explore.cterm_symbolic.implies.assert_not_called() +def _node_at_rung(rung: int, attrs: list[NodeAttr]) -> KCFG.Node: + chain: list[NodeVariant] = [] + if rung >= 1: + chain = [NodeVariant(Producer.INIT, None, term(1)), NodeVariant(Producer.BOOSTER_SIMPLIFY, 'r-b', term(2))] + if rung >= 2: + chain.append(NodeVariant(Producer.KORE_SIMPLIFY, 'r-k', term(3))) + return KCFG.Node(1, term(rung + 1), attrs, chain) + + +def test_recovery_rung() -> None: + assert recovery_rung(KCFG.Node(1, term(1))) == 0 + assert recovery_rung(_node_at_rung(0, [])) == 0 + assert recovery_rung(_node_at_rung(1, [])) == 1 + assert recovery_rung(_node_at_rung(2, [])) == 2 + + +_TASK_DATA: tuple[tuple[str, int, list[NodeAttr], RecoverTask], ...] = ( + # (rung, attrs, expected) — first matching §3d rule + ('rung0-fresh', 0, [], RecoverTask.TRY_BOOSTER), + ('rung0-tried', 0, [KCFGNodeAttr.BOOSTER_TRIED], RecoverTask.SIMPLIFY_BOOSTER), + ('rung1-fresh', 1, [], RecoverTask.TRY_BOOSTER), + ('rung1-tried', 1, [KCFGNodeAttr.BOOSTER_TRIED], RecoverTask.SIMPLIFY_KORE), + ('rung2-fresh', 2, [], RecoverTask.TRY_BOOSTER), + ('rung2-tried', 2, [KCFGNodeAttr.BOOSTER_TRIED], RecoverTask.TRY_KORE), +) + + +@pytest.mark.parametrize('test_id,rung,attrs,expected', _TASK_DATA, ids=[d[0] for d in _TASK_DATA]) +def test_recover_task_selection(test_id: str, rung: int, attrs: list[NodeAttr], expected: RecoverTask) -> None: + assert recover_task_for(_node_at_rung(rung, attrs)) is expected + + +def test_recover_task_noop_shortcircuit() -> None: + # After a no-op SIMPLIFY_BOOSTER, the term advanced to rung 1 but BOOSTER_TRIED stays set + # (commit's clear-iff-changed invariant), so the next task skips the redundant TRY_BOOSTER and + # goes straight to SIMPLIFY_KORE. + node = _node_at_rung(1, [KCFGNodeAttr.BOOSTER_TRIED]) + assert recover_task_for(node) is RecoverTask.SIMPLIFY_KORE + + def test_apr_proof_minimization_and_terminals() -> None: # 25 /-- X >=Int 5 --> 10 # 5 10 15 20 /-- X >=Int 0 --> 6 --> 8 From 78c0a0b860934ec7cb9b4c968c5ede51021903d1 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 30 May 2026 18:47:51 +0000 Subject: [PATCH 12/26] proof/reachability, tests/unit/test_proof: step_proof dispatch + recover-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 (cherry picked from commit 49ba6c0ca1b95fc529b65d5648a2452069d0a7d7) --- pyk/src/pyk/proof/reachability.py | 188 +++++++++++++++++++++++++++++- pyk/src/tests/unit/test_proof.py | 110 ++++++++++++++++- 2 files changed, 296 insertions(+), 2 deletions(-) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 5259f5fc1b..c9c30f8659 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -27,6 +27,7 @@ from pathlib import Path from typing import Any, Final, TypeVar + from ..cterm import CTerm from ..kast.outer import KDefinition, KFlatModuleList, KRuleLike from ..kcfg import KCFGExplore from ..kcfg.explore import KCFGExtendResult @@ -126,6 +127,59 @@ class APRProofStuckResult(APRProofResult): """ +@dataclass(frozen=True) +class LoggedCall: + """One kore RPC whose captured per-request log bundle the coordinator writes to disk (§5).""" + + request_id: str + log_entries: tuple[Any, ...] | None + + +@dataclass +class APRProofAddVariantResult(APRProofResult): + """Recover-mode: a re-simplification variant for `commit` to append via `KCFG.add_variant`.""" + + producer: Producer + cterm: CTerm + request_id: str | None + log_entries: tuple[Any, ...] | None + + +@dataclass +class APRProofRecoverNoProgressResult(APRProofResult): + """Recover-mode: a `try` made no progress; `commit` sets the per-backend attr (and may stuck).""" + + backend: str # 'booster' | 'kore' + subsume_indeterminate: bool + logged_calls: tuple[LoggedCall, ...] + + +@dataclass +class APRProofRecoverAdvanceResult(APRProofResult): + """Recover-mode: a `try` advanced the node; `commit` applies the extension and records a handoff. + + ``kore_request_id`` is set iff this was a kore execute — `commit` builds the ``execute`` + `KoreHandoff` from it once the successor node exists. + """ + + extension_to_apply: KCFGExtendResult + kore_request_id: str | None + logged_calls: tuple[LoggedCall, ...] + + +@dataclass +class APRProofRecoverCloseResult(APRProofResult): + """Recover-mode: a `try` closed the node by subsumption; `commit` covers and records a handoff. + + ``kore_request_id`` is set iff a kore implies closed it — `commit` builds the ``implies`` + `KoreHandoff` from it. + """ + + csubst: CSubst + kore_request_id: str | None + logged_calls: tuple[LoggedCall, ...] + + class SubsumptionCheck(ABC): """Tagged outcome of a subsumption (`implies`) check, replacing a bare ``CSubst | None``. @@ -906,6 +960,7 @@ def _check_subsume( target_node: KCFG.Node, proof_id: str, booster_only: bool | None = None, + haskell_logging: bool | None = None, ) -> SubsumptionCheck: target_cterm = target_node.cterm _LOGGER.debug(f'Checking subsumption into target state {proof_id}: {shorten_hashes((node.id, target_cterm))}') @@ -913,7 +968,11 @@ def _check_subsume( _LOGGER.info(f'Skipping full subsumption check because of fast may subsume check {proof_id}: {node.id}') return DecisiveInvalid() result = self.kcfg_explore.cterm_symbolic.implies( - node.cterm, target_cterm, assume_defined=self.assume_defined, booster_only_simplify=booster_only + node.cterm, + target_cterm, + assume_defined=self.assume_defined, + booster_only_simplify=booster_only, + haskell_logging=haskell_logging, ) if result.csubst is not None: _LOGGER.info(f'Subsumed into target node {proof_id}: {shorten_hashes((node.id, target_node.id))}') @@ -941,6 +1000,11 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: ) ] + # Recover-mode dispatches to a self-contained ladder step (terminal/subsume/execute are + # handled within, per the assigned task); the normal path below is left untouched (C13). + if step.recover_task is not None: + return self._recover_step(step, prior_loops) + # Check if the current node and target are terminal is_terminal = self.kcfg_explore.kcfg_semantics.is_terminal(step.node.cterm) target_is_terminal = self.kcfg_explore.kcfg_semantics.is_terminal(step.target.cterm) @@ -1043,6 +1107,128 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: ) ] + def _recover_step(self, step: APRProofStep, prior_loops: tuple[int, ...]) -> list[APRProofResult]: + task = step.recover_task + assert task is not None + if task in (RecoverTask.SIMPLIFY_BOOSTER, RecoverTask.SIMPLIFY_KORE): + return self._recover_simplify(step, prior_loops, booster_only=task is RecoverTask.SIMPLIFY_BOOSTER) + return self._recover_try(step, prior_loops, is_kore=task is RecoverTask.TRY_KORE) + + def _recover_simplify( + self, step: APRProofStep, prior_loops: tuple[int, ...], *, booster_only: bool + ) -> list[APRProofResult]: + variant = self.kcfg_explore.simplify_variant(step.node.cterm, booster_only=booster_only) + return [ + APRProofAddVariantResult( + node_id=step.node.id, + prior_loops_cache_update=prior_loops, + optimize_kcfg=self.optimize_kcfg, + producer=variant.producer, + cterm=variant.cterm, + request_id=variant.request_id, + log_entries=variant.log_entries, + ) + ] + + def _recover_try(self, step: APRProofStep, prior_loops: tuple[int, ...], *, is_kore: bool) -> list[APRProofResult]: + node = step.node + cs = self.kcfg_explore.cterm_symbolic + semantics = self.kcfg_explore.kcfg_semantics + # §3e: rung-0 booster tries (the happy path) are not logged; everything else is. + should_log = is_kore or recovery_rung(node) >= 1 + logged_calls: list[LoggedCall] = [] + + def capture() -> str | None: + rid = cs.last_request_id + if should_log and rid is not None: + logged_calls.append(LoggedCall(rid, cs.last_haskell_log_entries)) + return rid + + is_terminal = semantics.is_terminal(node.cterm) + target_is_terminal = semantics.is_terminal(step.target.cterm) + terminal_result: list[APRProofResult] = ( + [ + APRProofTerminalResult( + node_id=node.id, optimize_kcfg=self.optimize_kcfg, prior_loops_cache_update=prior_loops + ) + ] + if is_terminal + else [] + ) + + # Subsumption: TRY_BOOSTER always checks (booster-only); TRY_KORE checks (kore) only when the + # prior booster subsumption was indeterminate — otherwise we trust the decisive booster + # invalid and skip straight to kore-execute (§3b/§3c). + subsume_indeterminate = False + run_subsume = (is_terminal == target_is_terminal) and ( + not is_kore or KCFGNodeAttr.SUBSUME_INDETERMINATE in node.attrs + ) + if run_subsume: + subsumption = self._check_subsume( + node, step.target, proof_id=step.proof_id, booster_only=not is_kore, haskell_logging=should_log + ) + request_id = capture() + if isinstance(subsumption, Subsumed): + return terminal_result + [ + APRProofRecoverCloseResult( + node_id=node.id, + prior_loops_cache_update=prior_loops, + optimize_kcfg=self.optimize_kcfg, + csubst=subsumption.csubst, + kore_request_id=request_id if is_kore else None, + logged_calls=tuple(logged_calls), + ) + ] + subsume_indeterminate = isinstance(subsumption, Indeterminate) + + if is_terminal: + return terminal_result + + cut_rules = list(self.cut_point_rules) + if step.circularity and step.nonzero_depth: + cut_rules.append(step.circularity_rule_id) + # TRY_KORE takes a single kore step; TRY_BOOSTER uses the prover's normal depth. + execute_depth = 1 if is_kore else self.execute_depth + if not is_kore and step.circularity and not step.nonzero_depth: + execute_depth = 1 + + extend_results = self.kcfg_explore.extend_cterm( + node.cterm, + execute_depth=execute_depth, + cut_point_rules=cut_rules, + terminal_rules=self.terminal_rules, + module_name=step.module_name, + node_id=node.id, + booster_only_simplify=not is_kore, + raise_on_aborted=False, + haskell_logging=should_log, + ) + request_id = capture() + + # No progress: the worker does not stuck the node; commit sets the per-backend attr (C14). + if extend_results and isinstance(extend_results[0], NoProgress): + return [ + APRProofRecoverNoProgressResult( + node_id=node.id, + prior_loops_cache_update=prior_loops, + optimize_kcfg=self.optimize_kcfg, + backend='kore' if is_kore else 'booster', + subsume_indeterminate=subsume_indeterminate, + logged_calls=tuple(logged_calls), + ) + ] + # Progress: apply the first extension (extend-and-cache is disabled in recover-mode). + return [ + APRProofRecoverAdvanceResult( + node_id=node.id, + prior_loops_cache_update=prior_loops, + optimize_kcfg=self.optimize_kcfg, + extension_to_apply=extend_results[0], + kore_request_id=request_id if is_kore else None, + logged_calls=tuple(logged_calls), + ) + ] + def failure_info(self, proof: APRProof) -> FailureInfo: return APRFailureInfo.from_proof( proof, self.kcfg_explore, counterexample_info=self.counterexample_info, assume_defined=self.assume_defined diff --git a/pyk/src/tests/unit/test_proof.py b/pyk/src/tests/unit/test_proof.py index 1fa2951958..e5282c10e9 100644 --- a/pyk/src/tests/unit/test_proof.py +++ b/pyk/src/tests/unit/test_proof.py @@ -10,13 +10,18 @@ from pyk.kast.prelude.kbool import BOOL from pyk.kast.prelude.kint import intToken from pyk.kcfg.exploration import KCFGExplorationNodeAttr -from pyk.kcfg.kcfg import KCFG, KCFGNodeAttr, NodeVariant, Producer +from pyk.kcfg.explore import SimplifyVariant +from pyk.kcfg.kcfg import KCFG, KCFGNodeAttr, NodeVariant, NoProgress, Producer from pyk.proof import EqualityProof from pyk.proof.implies import EqualitySummary from pyk.proof.proof import CompositeSummary, Proof, ProofStatus from pyk.proof.reachability import ( APRFailureInfo, APRProof, + APRProofAddVariantResult, + APRProofRecoverAdvanceResult, + APRProofRecoverCloseResult, + APRProofRecoverNoProgressResult, APRProofStuckResult, APRProver, APRSummary, @@ -362,6 +367,109 @@ def test_recover_task_noop_shortcircuit() -> None: assert recover_task_for(node) is RecoverTask.SIMPLIFY_KORE +# --- step_proof recover dispatch (C13) ----------------------------------------------------------- + + +def _recover_prover(*, node: KCFG.Node) -> Mock: + """A Mock APRProver wired enough to exercise the unbound `_recover_*` methods.""" + prover = Mock() + prover.optimize_kcfg = False + prover.cut_point_rules = [] + prover.terminal_rules = [] + prover.execute_depth = None + prover.kcfg_explore.kcfg_semantics.is_terminal.return_value = False + prover.kcfg_explore.cterm_symbolic.last_request_id = 'req-1' + prover.kcfg_explore.cterm_symbolic.last_haskell_log_entries = ({'message': 'log'},) + return prover + + +def _step(node: KCFG.Node, task: RecoverTask) -> Mock: + return Mock(node=node, target=node, proof_id='p', circularity=False, nonzero_depth=True, recover_task=task) + + +def test_recover_simplify_yields_add_variant() -> None: + node = KCFG.Node(1, term(1)) + prover = _recover_prover(node=node) + prover.kcfg_explore.simplify_variant.return_value = SimplifyVariant( + Producer.BOOSTER_SIMPLIFY, term(2), 'req-s', ({'message': 'log'},) + ) + + result = APRProver._recover_simplify(prover, _step(node, RecoverTask.SIMPLIFY_BOOSTER), (), booster_only=True) + + assert len(result) == 1 + variant_result = result[0] + assert isinstance(variant_result, APRProofAddVariantResult) + assert variant_result.producer is Producer.BOOSTER_SIMPLIFY + assert variant_result.cterm == term(2) + assert variant_result.request_id == 'req-s' + + +def test_recover_try_booster_close() -> None: + node = KCFG.Node(1, term(1)) + prover = _recover_prover(node=node) + prover._check_subsume.return_value = Subsumed(CSubst()) + + result = APRProver._recover_try(prover, _step(node, RecoverTask.TRY_BOOSTER), (), is_kore=False) + + assert isinstance(result[-1], APRProofRecoverCloseResult) + # booster close → no kore handoff + assert result[-1].kore_request_id is None + + +def test_recover_try_booster_advance() -> None: + node = KCFG.Node(1, term(1)) + prover = _recover_prover(node=node) + prover._check_subsume.return_value = DecisiveInvalid() + prover.kcfg_explore.extend_cterm.return_value = [Mock()] # not NoProgress ⇒ advance + + result = APRProver._recover_try(prover, _step(node, RecoverTask.TRY_BOOSTER), (), is_kore=False) + + assert isinstance(result[0], APRProofRecoverAdvanceResult) + assert result[0].kore_request_id is None + + +def test_recover_try_booster_no_progress_carries_indeterminate() -> None: + node = KCFG.Node(1, term(1)) + prover = _recover_prover(node=node) + prover._check_subsume.return_value = Indeterminate() + prover.kcfg_explore.extend_cterm.return_value = [NoProgress()] + + result = APRProver._recover_try(prover, _step(node, RecoverTask.TRY_BOOSTER), (), is_kore=False) + + no_progress = result[0] + assert isinstance(no_progress, APRProofRecoverNoProgressResult) + assert no_progress.backend == 'booster' + assert no_progress.subsume_indeterminate is True + + +def test_recover_try_kore_skips_implies_without_indeterminate_flag() -> None: + # rung-2 node without SUBSUME_INDETERMINATE: trust the decisive booster invalid, go to execute. + node = KCFG.Node(1, term(1), [KCFGNodeAttr.BOOSTER_TRIED]) + prover = _recover_prover(node=node) + prover.kcfg_explore.extend_cterm.return_value = [Mock()] + + result = APRProver._recover_try(prover, _step(node, RecoverTask.TRY_KORE), (), is_kore=True) + + prover._check_subsume.assert_not_called() + advance = result[0] + assert isinstance(advance, APRProofRecoverAdvanceResult) + # kore execute advance → handoff request id captured + assert advance.kore_request_id == 'req-1' + + +def test_recover_try_kore_close_records_handoff_id() -> None: + node = KCFG.Node(1, term(1), [KCFGNodeAttr.SUBSUME_INDETERMINATE]) + prover = _recover_prover(node=node) + prover._check_subsume.return_value = Subsumed(CSubst()) + + result = APRProver._recover_try(prover, _step(node, RecoverTask.TRY_KORE), (), is_kore=True) + + prover._check_subsume.assert_called_once() + close = result[-1] + assert isinstance(close, APRProofRecoverCloseResult) + assert close.kore_request_id == 'req-1' # kore implies closed ⇒ handoff id set + + def test_apr_proof_minimization_and_terminals() -> None: # 25 /-- X >=Int 5 --> 10 # 5 10 15 20 /-- X >=Int 0 --> 6 --> 8 From f90345e654206e784cbeb85a6da41e2fee219c52 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 30 May 2026 18:52:28 +0000 Subject: [PATCH 13/26] proof/reachability, tests/unit/test_proof: commit transitions for recover-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 (cherry picked from commit 7f4f82b39c883d593fdf39f7aa5bb4365ae1136a) --- pyk/src/pyk/proof/reachability.py | 88 ++++++++++++++- pyk/src/tests/unit/test_proof.py | 174 +++++++++++++++++++++++++++++- 2 files changed, 260 insertions(+), 2 deletions(-) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index c9c30f8659..156b72aaad 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -15,7 +15,7 @@ from ..kast.prelude.ml import mlAnd, mlTop from ..kcfg import KCFG, KCFGStore from ..kcfg.exploration import KCFGExploration -from ..kcfg.kcfg import KCFGNodeAttr, NoProgress, Producer +from ..kcfg.kcfg import KCFGNodeAttr, KoreHandoff, NoProgress, Producer from ..kore.rpc import LogEntry, client_label from ..ktool.claim_index import ClaimIndex from ..utils import FrozenDict, ensure_dir_path, hash_str, shorten_hashes, single @@ -389,11 +389,75 @@ def commit(self, result: APRProofResult) -> None: # Sole site that marks a node stuck: the coordinator owns this judgment (C6). _LOGGER.info(f'Stuck node {self.id}: {result.node_id}') self.kcfg.add_stuck(result.node_id) + elif isinstance(result, APRProofAddVariantResult): + self._commit_add_variant(result) + elif isinstance(result, APRProofRecoverNoProgressResult): + self._commit_recover_no_progress(result) + elif isinstance(result, APRProofRecoverAdvanceResult): + self.kcfg.extend( + extend_result=result.extension_to_apply, + optimize_kcfg=result.optimize_kcfg, + node=self.kcfg.node(result.node_id), + logs=self.logs, + ) + if result.kore_request_id is not None: + target_id = self._recover_successor_id(result.node_id) + self.kcfg.add_kore_handoff( + KoreHandoff( + source=result.node_id, target=target_id, flavour='execute', request_id=result.kore_request_id + ) + ) + elif isinstance(result, APRProofRecoverCloseResult): + self.kcfg.create_cover(result.node_id, self.target, csubst=result.csubst) + if result.kore_request_id is not None: + self.kcfg.add_kore_handoff( + KoreHandoff( + source=result.node_id, target=self.target, flavour='implies', request_id=result.kore_request_id + ) + ) elif isinstance(result, APRProofBoundedResult): self.add_bounded(result.node_id) else: raise ValueError(f'Incorrect result type, expected APRProofResult: {result}') + def _commit_add_variant(self, result: APRProofAddVariantResult) -> None: + # Clear-iff-changed invariant (§3d): clear the per-rung try attrs only when the simplify + # actually changed the term, so the simplified node is re-tried with booster. A no-op + # variant leaves BOOSTER_TRIED set, so the next task is the next simplify rung (the no-op + # short-circuit) rather than a futile TRY_BOOSTER on the byte-identical term. + prev_cterm = self.kcfg.node(result.node_id).cterm + self.kcfg.add_variant(result.node_id, result.producer, result.cterm, result.request_id) + if result.cterm != prev_cterm: + self.kcfg.discard_attr(result.node_id, KCFGNodeAttr.BOOSTER_TRIED) + self.kcfg.discard_attr(result.node_id, KCFGNodeAttr.SUBSUME_INDETERMINATE) + + def _commit_recover_no_progress(self, result: APRProofRecoverNoProgressResult) -> None: + if result.backend == 'kore': + self.kcfg.add_attr(result.node_id, KCFGNodeAttr.KORE_TRIED) + else: + self.kcfg.add_attr(result.node_id, KCFGNodeAttr.BOOSTER_TRIED) + if result.subsume_indeterminate: + self.kcfg.add_attr(result.node_id, KCFGNodeAttr.SUBSUME_INDETERMINATE) + # Rung-2 exhaustion: booster simplify, kore simplify, booster try, and kore try all failed to + # advance the node — a genuine dead-end. The coordinator (and only it) marks it stuck (C6), + # tagged so the diagnostic can distinguish it from an ordinary stuck. + attrs = self.kcfg.node(result.node_id).attrs + if KCFGNodeAttr.BOOSTER_TRIED in attrs and KCFGNodeAttr.KORE_TRIED in attrs: + self.kcfg.add_attr(result.node_id, KCFGNodeAttr.BOTH_BACKENDS_FAILED) + _LOGGER.info(f'Both backends failed, stuck node {self.id}: {result.node_id}') + self.kcfg.add_stuck(result.node_id) + + def _recover_successor_id(self, node_id: int) -> int: + """Resolve the kore execute handoff target: the (min) new successor of ``node_id``. + + Falls back to ``node_id`` itself if the node was merged away under ``optimize_kcfg`` — the + ``request_id`` remains the durable join key onto the stored logs in that case. + """ + if self.kcfg.get_node(node_id) is None: + return node_id + targets = [target_id for succ in self.kcfg.successors(node_id) for target_id in succ.target_ids] + return min(targets) if targets else node_id + def nonzero_depth(self, node: KCFG.Node) -> bool: return not self.kcfg.zero_depth_between(self.init, node.id) @@ -1181,7 +1245,29 @@ def capture() -> str | None: ] subsume_indeterminate = isinstance(subsumption, Indeterminate) + # A terminal node is finalized as terminal — and so, if unsubsumed, declared failing — only + # once a kore implies has had its say. Normal mode's proxy implies (booster + kore fallback) + # closes terminal end-states that booster alone cannot; recover-mode must match that or it + # regresses passing proofs into failures (a terminal node that booster cannot subsume but + # kore can would otherwise be marked terminal at rung 0 and drop out of `pending` before the + # ladder ever reaches TRY_KORE). So a non-kore try whose subsumption check ran and did not + # close escalates instead: it records BOOSTER_TRIED + SUBSUME_INDETERMINATE (forced, even on + # a decisive booster invalid — for a terminal node we always want kore's second opinion + # before failing it) so the node climbs to TRY_KORE's kore implies. Only the kore try (or a + # terminal/non-terminal target mismatch that skipped the check, exactly as normal mode skips + # it) finalizes a terminal node here. if is_terminal: + if not is_kore and run_subsume: + return [ + APRProofRecoverNoProgressResult( + node_id=node.id, + prior_loops_cache_update=prior_loops, + optimize_kcfg=self.optimize_kcfg, + backend='booster', + subsume_indeterminate=True, + logged_calls=tuple(logged_calls), + ) + ] return terminal_result cut_rules = list(self.cut_point_rules) diff --git a/pyk/src/tests/unit/test_proof.py b/pyk/src/tests/unit/test_proof.py index e5282c10e9..8e4dd1ab6d 100644 --- a/pyk/src/tests/unit/test_proof.py +++ b/pyk/src/tests/unit/test_proof.py @@ -11,7 +11,7 @@ from pyk.kast.prelude.kint import intToken from pyk.kcfg.exploration import KCFGExplorationNodeAttr from pyk.kcfg.explore import SimplifyVariant -from pyk.kcfg.kcfg import KCFG, KCFGNodeAttr, NodeVariant, NoProgress, Producer +from pyk.kcfg.kcfg import KCFG, KCFGNodeAttr, KoreHandoff, NodeVariant, NoProgress, Producer, Step from pyk.proof import EqualityProof from pyk.proof.implies import EqualitySummary from pyk.proof.proof import CompositeSummary, Proof, ProofStatus @@ -23,6 +23,7 @@ APRProofRecoverCloseResult, APRProofRecoverNoProgressResult, APRProofStuckResult, + APRProofTerminalResult, APRProver, APRSummary, DecisiveInvalid, @@ -42,6 +43,7 @@ from pytest import TempPathFactory + from pyk.cterm import CTerm from pyk.kcfg.kcfg import NodeAttr from pyk.proof.reachability import SubsumptionCheck @@ -470,6 +472,176 @@ def test_recover_try_kore_close_records_handoff_id() -> None: assert close.kore_request_id == 'req-1' # kore implies closed ⇒ handoff id set +@pytest.mark.parametrize('subsumption', [Indeterminate(), DecisiveInvalid()], ids=['indeterminate', 'decisive-invalid']) +def test_recover_try_terminal_booster_escalates_instead_of_failing(subsumption: object) -> None: + # Regression (recover-mode parity): a terminal node whose booster subsumption does not close must + # NOT be finalized as terminal at the booster rung — that drops it out of `pending` before the + # ladder can reach a kore implies, regressing proofs that normal mode's kore-capable proxy implies + # would close. Both a booster `Indeterminate` and a decisive booster `invalid` escalate: for a + # terminal node we always want kore's second opinion before declaring it failing. + node = KCFG.Node(1, term(1)) + prover = _recover_prover(node=node) + prover.kcfg_explore.kcfg_semantics.is_terminal.return_value = True + prover._check_subsume.return_value = subsumption + + result = APRProver._recover_try(prover, _step(node, RecoverTask.TRY_BOOSTER), (), is_kore=False) + + # Not finalized as terminal; escalates so the node climbs to TRY_KORE's kore implies. + assert not any(isinstance(r, APRProofTerminalResult) for r in result) + no_progress = result[0] + assert isinstance(no_progress, APRProofRecoverNoProgressResult) + assert no_progress.backend == 'booster' + assert no_progress.subsume_indeterminate is True + prover.kcfg_explore.extend_cterm.assert_not_called() # a terminal node is never executed + + +def test_recover_try_terminal_kore_finalizes_when_implies_fails() -> None: + # The kore rung is the top of the ladder: once the kore implies on a terminal node also fails to + # close, the node is legitimately finalized as terminal (and so, unsubsumed, becomes failing). + node = KCFG.Node(1, term(1), [KCFGNodeAttr.SUBSUME_INDETERMINATE]) + prover = _recover_prover(node=node) + prover.kcfg_explore.kcfg_semantics.is_terminal.return_value = True + prover._check_subsume.return_value = DecisiveInvalid() + + result = APRProver._recover_try(prover, _step(node, RecoverTask.TRY_KORE), (), is_kore=True) + + prover._check_subsume.assert_called_once() + assert len(result) == 1 + assert isinstance(result[0], APRProofTerminalResult) + prover.kcfg_explore.extend_cterm.assert_not_called() + + +# --- commit recover transitions (C14) ------------------------------------------------------------ + + +def _recover_proof() -> tuple[APRProof, int]: + kcfg = KCFG() + n_init = kcfg.create_node(term(1)) + n_target = kcfg.create_node(term(2)) + n = kcfg.create_node(term(3)) + proof = APRProof(id='rec', kcfg=kcfg, terminal=[], init=n_init.id, target=n_target.id, logs={}) + return proof, n.id + + +def _no_progress(node_id: int, backend: str, indeterminate: bool = False) -> APRProofRecoverNoProgressResult: + return APRProofRecoverNoProgressResult( + node_id=node_id, + prior_loops_cache_update=(), + optimize_kcfg=False, + backend=backend, + subsume_indeterminate=indeterminate, + logged_calls=(), + ) + + +def _add_variant(node_id: int, producer: Producer, cterm: CTerm) -> APRProofAddVariantResult: + return APRProofAddVariantResult( + node_id=node_id, + prior_loops_cache_update=(), + optimize_kcfg=False, + producer=producer, + cterm=cterm, + request_id='r', + log_entries=None, + ) + + +def test_commit_no_progress_sets_booster_tried_and_indeterminate() -> None: + proof, nid = _recover_proof() + proof.commit(_no_progress(nid, 'booster', indeterminate=True)) + attrs = proof.kcfg.node(nid).attrs + assert KCFGNodeAttr.BOOSTER_TRIED in attrs + assert KCFGNodeAttr.SUBSUME_INDETERMINATE in attrs + assert not proof.kcfg.is_stuck(nid) + + +def test_commit_add_variant_clear_iff_changed() -> None: + proof, nid = _recover_proof() + proof.commit(_no_progress(nid, 'booster', indeterminate=True)) + + # No-op simplify (term unchanged): BOOSTER_TRIED stays set → short-circuit to next rung + proof.commit(_add_variant(nid, Producer.BOOSTER_SIMPLIFY, term(3))) + assert KCFGNodeAttr.BOOSTER_TRIED in proof.kcfg.node(nid).attrs + assert recovery_rung(proof.kcfg.node(nid)) == 1 + + # A term-changing simplify clears the per-rung try attrs + proof.commit(_add_variant(nid, Producer.KORE_SIMPLIFY, term(99))) + cleared = proof.kcfg.node(nid).attrs + assert KCFGNodeAttr.BOOSTER_TRIED not in cleared + assert KCFGNodeAttr.SUBSUME_INDETERMINATE not in cleared + assert recovery_rung(proof.kcfg.node(nid)) == 2 + + +def test_commit_full_ladder_to_both_backends_failed() -> None: + proof, nid = _recover_proof() + # rung 0: booster try fails (indeterminate), booster simplify changes the term → rung 1 + proof.commit(_no_progress(nid, 'booster', indeterminate=True)) + proof.commit(_add_variant(nid, Producer.BOOSTER_SIMPLIFY, term(10))) + # rung 1: booster try fails, kore simplify changes the term → rung 2 + proof.commit(_no_progress(nid, 'booster')) + proof.commit(_add_variant(nid, Producer.KORE_SIMPLIFY, term(20))) + # rung 2: booster try fails, then kore try fails → both backends exhausted + proof.commit(_no_progress(nid, 'booster')) + assert not proof.kcfg.is_stuck(nid) + proof.commit(_no_progress(nid, 'kore')) + + node = proof.kcfg.node(nid) + assert KCFGNodeAttr.BOTH_BACKENDS_FAILED in node.attrs + assert proof.kcfg.is_stuck(nid) + + +def test_commit_recover_close_records_implies_handoff() -> None: + proof, nid = _recover_proof() + proof.commit( + APRProofRecoverCloseResult( + node_id=nid, + prior_loops_cache_update=(), + optimize_kcfg=False, + csubst=CSubst(), + kore_request_id='r-imp', + logged_calls=(), + ) + ) + assert proof.kcfg.kore_handoffs == [ + KoreHandoff(source=nid, target=proof.target, flavour='implies', request_id='r-imp') + ] + + +def test_commit_recover_advance_records_execute_handoff() -> None: + proof, nid = _recover_proof() + proof.commit( + APRProofRecoverAdvanceResult( + node_id=nid, + prior_loops_cache_update=(), + optimize_kcfg=False, + extension_to_apply=Step(term(50), 1, (), []), + kore_request_id='r-exec', + logged_calls=(), + ) + ) + handoffs = proof.kcfg.kore_handoffs + assert len(handoffs) == 1 + assert handoffs[0].flavour == 'execute' + assert handoffs[0].source == nid + assert handoffs[0].request_id == 'r-exec' + + +def test_commit_recover_advance_no_handoff_for_booster() -> None: + # A booster advance (kore_request_id None) records no handoff. + proof, nid = _recover_proof() + proof.commit( + APRProofRecoverAdvanceResult( + node_id=nid, + prior_loops_cache_update=(), + optimize_kcfg=False, + extension_to_apply=Step(term(50), 1, (), []), + kore_request_id=None, + logged_calls=(), + ) + ) + assert proof.kcfg.kore_handoffs == [] + + def test_apr_proof_minimization_and_terminals() -> None: # 25 /-- X >=Int 5 --> 10 # 5 10 15 20 /-- X >=Int 0 --> 6 --> 8 From 790019df2b199b372638bbe7304d4062fa252394 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 30 May 2026 18:54:55 +0000 Subject: [PATCH 14/26] proof/reachability, tests/unit/test_proof: write recover-logs/{request_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 (cherry picked from commit f1fe0a567f7fd88744070ee69d65480cb153b37f) --- pyk/src/pyk/proof/reachability.py | 23 ++++++++++++++ pyk/src/tests/unit/test_proof.py | 53 +++++++++++++++++++++++++++++++ 2 files changed, 76 insertions(+) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 156b72aaad..83541f1464 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -407,6 +407,7 @@ def commit(self, result: APRProofResult) -> None: source=result.node_id, target=target_id, flavour='execute', request_id=result.kore_request_id ) ) + self._write_recover_logs(result.logged_calls) elif isinstance(result, APRProofRecoverCloseResult): self.kcfg.create_cover(result.node_id, self.target, csubst=result.csubst) if result.kore_request_id is not None: @@ -415,6 +416,7 @@ def commit(self, result: APRProofResult) -> None: source=result.node_id, target=self.target, flavour='implies', request_id=result.kore_request_id ) ) + self._write_recover_logs(result.logged_calls) elif isinstance(result, APRProofBoundedResult): self.add_bounded(result.node_id) else: @@ -430,6 +432,8 @@ def _commit_add_variant(self, result: APRProofAddVariantResult) -> None: if result.cterm != prev_cterm: self.kcfg.discard_attr(result.node_id, KCFGNodeAttr.BOOSTER_TRIED) self.kcfg.discard_attr(result.node_id, KCFGNodeAttr.SUBSUME_INDETERMINATE) + if result.request_id is not None and result.log_entries is not None: + self._write_recover_logs((LoggedCall(result.request_id, result.log_entries),)) def _commit_recover_no_progress(self, result: APRProofRecoverNoProgressResult) -> None: if result.backend == 'kore': @@ -446,6 +450,7 @@ def _commit_recover_no_progress(self, result: APRProofRecoverNoProgressResult) - self.kcfg.add_attr(result.node_id, KCFGNodeAttr.BOTH_BACKENDS_FAILED) _LOGGER.info(f'Both backends failed, stuck node {self.id}: {result.node_id}') self.kcfg.add_stuck(result.node_id) + self._write_recover_logs(result.logged_calls) def _recover_successor_id(self, node_id: int) -> int: """Resolve the kore execute handoff target: the (min) new successor of ``node_id``. @@ -458,6 +463,24 @@ def _recover_successor_id(self, node_id: int) -> int: targets = [target_id for succ in self.kcfg.successors(node_id) for target_id in succ.target_ids] return min(targets) if targets else node_id + def _write_recover_logs(self, logged_calls: Iterable[LoggedCall]) -> None: + """Write one ``recover-logs/{request_id}.jsonl`` per logged kore call (§5). + + Each line is one captured log entry in ``--log-format json`` shape, so the file feeds + straight into ``parse_kore_log``. No-ops when the proof is in-memory (no ``proof_subdir``) + or a call captured no entries. Disk writes stay on the coordinator (main) thread. + """ + if self.proof_subdir is None: + return + log_dir = self.proof_subdir / 'recover-logs' + for call in logged_calls: + if call.log_entries is None: + continue + ensure_dir_path(log_dir) + (log_dir / f'{call.request_id}.jsonl').write_text( + '\n'.join(json.dumps(entry) for entry in call.log_entries) + ) + def nonzero_depth(self, node: KCFG.Node) -> bool: return not self.kcfg.zero_depth_between(self.init, node.id) diff --git a/pyk/src/tests/unit/test_proof.py b/pyk/src/tests/unit/test_proof.py index 8e4dd1ab6d..1d13fa7ae2 100644 --- a/pyk/src/tests/unit/test_proof.py +++ b/pyk/src/tests/unit/test_proof.py @@ -1,5 +1,6 @@ from __future__ import annotations +import json from typing import TYPE_CHECKING from unittest.mock import Mock @@ -28,6 +29,7 @@ APRSummary, DecisiveInvalid, Indeterminate, + LoggedCall, RecoverTask, Subsumed, recover_task_for, @@ -642,6 +644,57 @@ def test_commit_recover_advance_no_handoff_for_booster() -> None: assert proof.kcfg.kore_handoffs == [] +def test_commit_writes_recover_logs(proof_dir: Path) -> None: + kcfg = KCFG() + n_init = kcfg.create_node(term(1)) + n_target = kcfg.create_node(term(2)) + n = kcfg.create_node(term(3)) + proof = APRProof(id='rec', kcfg=kcfg, terminal=[], init=n_init.id, target=n_target.id, logs={}, proof_dir=proof_dir) + entries = ({'context': ['proxy'], 'message': 'x'}, {'rule_id': 'abc', 'pre_hash': 'd'}) + + proof.commit( + APRProofRecoverNoProgressResult( + node_id=n.id, + prior_loops_cache_update=(), + optimize_kcfg=False, + backend='kore', + subsume_indeterminate=False, + logged_calls=(LoggedCall('claim-007', entries),), + ) + ) + + assert proof.proof_subdir is not None + log_file = proof.proof_subdir / 'recover-logs' / 'claim-007.jsonl' + assert log_file.exists() + parsed = [json.loads(line) for line in log_file.read_text().splitlines()] + assert parsed == [dict(entry) for entry in entries] + + +def test_commit_recover_logs_skipped_when_no_entries(proof_dir: Path) -> None: + kcfg = KCFG() + n_init = kcfg.create_node(term(1)) + n_target = kcfg.create_node(term(2)) + n = kcfg.create_node(term(3)) + proof = APRProof( + id='rec2', kcfg=kcfg, terminal=[], init=n_init.id, target=n_target.id, logs={}, proof_dir=proof_dir + ) + + # A call that captured no entries (None) writes no file. + proof.commit( + APRProofRecoverNoProgressResult( + node_id=n.id, + prior_loops_cache_update=(), + optimize_kcfg=False, + backend='booster', + subsume_indeterminate=False, + logged_calls=(LoggedCall('claim-008', None),), + ) + ) + + assert proof.proof_subdir is not None + assert not (proof.proof_subdir / 'recover-logs' / 'claim-008.jsonl').exists() + + def test_apr_proof_minimization_and_terminals() -> None: # 25 /-- X >=Int 5 --> 10 # 5 10 15 20 /-- X >=Int 0 --> 6 --> 8 From fa5a16e429655e163a706f637fd27506c37311b9 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 30 May 2026 19:00:48 +0000 Subject: [PATCH 15/26] cli/pyk, proof/prove_rpc, tests/unit/test_toml_args: --booster-recover-mode through ProveOptions to APRProver MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 (cherry picked from commit 3075366ae1167fcc137e1170bfbeb8f5ed1bc8c6) --- pyk/src/pyk/cli/pyk.py | 13 +++++++++++++ pyk/src/pyk/proof/prove_rpc.py | 9 ++++++++- pyk/src/tests/unit/test_toml_args.py | 13 ++++++++++++- 3 files changed, 33 insertions(+), 2 deletions(-) diff --git a/pyk/src/pyk/cli/pyk.py b/pyk/src/pyk/cli/pyk.py index 8a23469ed8..4ff9dbd3b7 100644 --- a/pyk/src/pyk/cli/pyk.py +++ b/pyk/src/pyk/cli/pyk.py @@ -319,6 +319,7 @@ class ProveOptions(LoggingOptions, SpecOptions, SaveDirOptions): assume_defined: bool show_kcfg: bool haskell_logging: bool + booster_recover_mode: bool @staticmethod def default() -> dict[str, Any]: @@ -332,6 +333,7 @@ def default() -> dict[str, Any]: 'assume_defined': False, 'show_kcfg': False, 'haskell_logging': False, + 'booster_recover_mode': False, } @staticmethod @@ -533,6 +535,17 @@ def create_argument_parser() -> ArgumentParser: ' Requires --save-directory.' ), ) + prove_args.add_argument( + '--booster-recover-mode', + dest='booster_recover_mode', + default=None, + action='store_true', + help=( + 'Run the reachability prover booster-only, escalating to Kore (re-simplification then' + ' the Kore operation) only where booster cannot make progress, and record in the KCFG' + ' exactly where Kore did work (variants + kore_handoffs) for diagnostic attribution.' + ), + ) show_args = pyk_args_command.add_parser( 'show', diff --git a/pyk/src/pyk/proof/prove_rpc.py b/pyk/src/pyk/proof/prove_rpc.py index df01ad30b4..6766d3fe29 100644 --- a/pyk/src/pyk/proof/prove_rpc.py +++ b/pyk/src/pyk/proof/prove_rpc.py @@ -52,6 +52,7 @@ def prove_rpc(self, options: ProveOptions) -> list[Proof]: max_depth=options.max_depth, save_directory=options.save_directory, max_iterations=options.max_iterations, + recover_mode=options.booster_recover_mode, ) for claim in all_claims ] @@ -63,6 +64,7 @@ def _prove_claim_rpc( max_depth: int | None = None, save_directory: Path | None = None, max_iterations: int | None = None, + recover_mode: bool = False, ) -> Proof: definition = self._kprove.definition @@ -90,7 +92,12 @@ def _prove_claim_rpc( prover = ImpliesProver(proof, kcfg_explore, assume_defined=assume_defined) else: assert type(proof) is APRProof - prover = APRProver(kcfg_explore, execute_depth=max_depth, assume_defined=assume_defined) + prover = APRProver( + kcfg_explore, + execute_depth=max_depth, + assume_defined=assume_defined, + recover_mode=recover_mode, + ) prover.advance_proof(proof, max_iterations=max_iterations) # type: ignore [arg-type] if proof.passed: diff --git a/pyk/src/tests/unit/test_toml_args.py b/pyk/src/tests/unit/test_toml_args.py index 455e838eed..2b9bbcab35 100644 --- a/pyk/src/tests/unit/test_toml_args.py +++ b/pyk/src/tests/unit/test_toml_args.py @@ -5,7 +5,7 @@ from os import PathLike from typing import TYPE_CHECKING -from pyk.cli.pyk import PrintInput, create_argument_parser, parse_toml_args +from pyk.cli.pyk import PrintInput, ProveOptions, create_argument_parser, parse_toml_args from .utils import TEST_DATA_DIR @@ -45,6 +45,17 @@ def test_print_input() -> None: assert not args_dict['minimize'] +def test_prove_booster_recover_mode_flag() -> None: + parser = create_argument_parser() + + # The flag parses to True and is off (None at the arg layer, False in ProveOptions) by default + args = parser.parse_args(['prove', str(TEST_TOML), '--booster-recover-mode']) + assert args.booster_recover_mode is True + args_default = parser.parse_args(['prove', str(TEST_TOML)]) + assert args_default.booster_recover_mode is None + assert ProveOptions.default()['booster_recover_mode'] is False + + def test_prove_legacy_kargs() -> None: parser = create_argument_parser() cmd_args = [ From e7787612e3e3ae384bf6728b873eb93a64aea743 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 30 May 2026 19:03:26 +0000 Subject: [PATCH 16/26] tests/integration/proof/test_imp: recover-mode prove of known IMP claims MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 (cherry picked from commit 80e56273c4388ff6811685edbda53ec6ef144849) --- pyk/src/tests/integration/proof/test_imp.py | 35 +++++++++++++++++++++ 1 file changed, 35 insertions(+) diff --git a/pyk/src/tests/integration/proof/test_imp.py b/pyk/src/tests/integration/proof/test_imp.py index 65be2ca7d4..7899151159 100644 --- a/pyk/src/tests/integration/proof/test_imp.py +++ b/pyk/src/tests/integration/proof/test_imp.py @@ -902,6 +902,41 @@ def test_assume_defined( # Then assert actual == expected + @pytest.mark.parametrize('claim_id', ['addition-1', 'addition-2', 'pre-branch-proved']) + def test_booster_recover_mode_prove( + self, + kprove: KProve, + kcfg_explore: KCFGExplore, + claim_id: str, + tmp_path_factory: TempPathFactory, + ) -> None: + # Recover-mode must prove as well as the normal prover: a claim that passes normally still + # passes booster-only-with-Kore-escalation, and its diagnostic state stays well-formed. + proof_dir = tmp_path_factory.mktemp(f'recover_tmp_proofs-{claim_id}') + spec_module = 'IMP-SIMPLE-SPEC' + spec_modules = kprove.parse_modules(K_FILES / 'imp-simple-spec.k', module_name=spec_module) + spec_label = f'{spec_module}.{claim_id}' + proofs = APRProof.from_spec_modules( + kprove.definition, spec_modules, spec_labels=[spec_label], logs={}, proof_dir=proof_dir + ) + proof = single([p for p in proofs if p.id == spec_label]) + for subproof in proof.subproofs: + subproof.admit() + subproof.write_proof_data() + + prover = APRProver(kcfg_explore=kcfg_explore, execute_depth=20, recover_mode=True) + prover.advance_proof(proof) + + assert proof.status == ProofStatus.PASSED + # Every recorded handoff/variant must name a Kore-producer with a request-id join key; a + # node's canonical term always matches its variant chain's tail (invariant of add_variant). + for handoff in proof.kcfg.kore_handoffs: + assert handoff.flavour in ('execute', 'implies') + assert handoff.request_id + for node in proof.kcfg.nodes: + if node.variants: + assert node.variants[-1].cterm == node.cterm + @pytest.mark.parametrize( 'test_id,spec_file,spec_module,claim_id,max_iterations,max_depth,cut_rules,admit_deps,proof_status,expected_leaf_number', APR_PROVE_TEST_DATA, From a36c9327cac97ab0bfa46b0daf5233661e9b75c1 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 1 Jun 2026 02:58:49 +0000 Subject: [PATCH 17/26] kore/rpc, cterm/symbolic, tests/unit/{cterm/test_symbolic,kore/test_client}: map kore Aborted (code 6) to AbortedError, treat aborted implies as indeterminate MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 (cherry picked from commit ec5541b363cce4babc6da0729f04bca18d0b5834) --- pyk/src/pyk/cterm/symbolic.py | 10 ++++++ pyk/src/pyk/kore/rpc.py | 37 +++++++++++++++++++++++ pyk/src/tests/unit/cterm/test_symbolic.py | 20 +++++++++++- pyk/src/tests/unit/kore/test_client.py | 14 +++++++++ 4 files changed, 80 insertions(+), 1 deletion(-) diff --git a/pyk/src/pyk/cterm/symbolic.py b/pyk/src/pyk/cterm/symbolic.py index bf2b82d4b8..c62e97cbae 100644 --- a/pyk/src/pyk/cterm/symbolic.py +++ b/pyk/src/pyk/cterm/symbolic.py @@ -14,6 +14,7 @@ from ..kast.pretty import PrettyPrinter from ..konvert import kast_to_kore, kflatmodule_to_kore, kore_to_kast from ..kore.rpc import ( + AbortedError, AbortedResult, KoreClient, KoreExecLogFormat, @@ -337,6 +338,15 @@ def implies( ) except SmtSolverError as err: raise self._smt_solver_error(err) from err + except AbortedError as err: + # kore-implies aborted because it could not decide the implication (e.g. constraints + # the engine cannot discharge). Surface it as an indeterminate, not-subsumed result — + # uniform with how booster-implies reports a MatchIndeterminate (`indeterminate=True`) — + # so callers (notably recover-mode's TRY_KORE escalation, which calls kore-implies + # directly and so sees the raw abort the proxy would otherwise absorb) treat it as + # "unknown" instead of crashing. + _LOGGER.warning(f'implies aborted, treating as indeterminate: {err.data}') + return CTermImplies(None, (), None, (), indeterminate=True) self._capture_haskell_log(result.haskell_log_entries) if not result.valid: diff --git a/pyk/src/pyk/kore/rpc.py b/pyk/src/pyk/kore/rpc.py index 4b7aba0bee..408f74d12e 100644 --- a/pyk/src/pyk/kore/rpc.py +++ b/pyk/src/pyk/kore/rpc.py @@ -454,6 +454,39 @@ def __init__(self, error: str, pattern: Pattern): super().__init__(f'SMT solver error: {self.error} Pattern: {self.pattern.text}') +@final +@dataclass +class AbortedError(KoreClientError): + """A backend engine aborted the request because it could not decide it (JSON-RPC ``code: 6``). + + The backend raises this when a request carried something the engine does not know how to + process — e.g. an ``implies`` whose constraints it cannot discharge. It is a "couldn't + determine," not a decisive verdict, so callers should treat it as indeterminate rather than as + a definite answer. ``data`` is the abort-reason text (e.g. ``"unknown constraints"``). + """ + + data: str + + def __init__(self, data: str): + self.data = data + super().__init__(f'Backend aborted: {self.data}') + + +@final +@dataclass +class MultipleStatesError(KoreClientError): + """The backend returned multiple states where one was expected (JSON-RPC ``code: 7``). + + ``data`` is the accompanying reason text. + """ + + data: str + + def __init__(self, data: str): + self.data = data + super().__init__(f'Multiple states: {self.data}') + + @final @dataclass class DefaultError(KoreClientError): @@ -1056,6 +1089,10 @@ def _error(self, err: JsonRpcError) -> KoreClientError: return ImplicationError(error=err.data['error'], context=err.data['context']) case 5: return SmtSolverError(error=err.data['error'], pattern=kore_term(err.data['term'])) + case 6: + return AbortedError(data=err.data) + case 7: + return MultipleStatesError(data=err.data) case 8: return InvalidModuleError(error=err.data['error'], context=err.data.get('context')) case 9: diff --git a/pyk/src/tests/unit/cterm/test_symbolic.py b/pyk/src/tests/unit/cterm/test_symbolic.py index 9fd10c4143..4dac195178 100644 --- a/pyk/src/tests/unit/cterm/test_symbolic.py +++ b/pyk/src/tests/unit/cterm/test_symbolic.py @@ -9,7 +9,7 @@ from pyk.cterm.symbolic import HASKELL_LOGGING_ENTRIES, CTermSymbolic, cterm_symbolic from pyk.kast.prelude.ml import mlTop from pyk.kore.prelude import int_dv -from pyk.kore.rpc import AbortedResult, ImpliesResult, State, StuckResult +from pyk.kore.rpc import AbortedError, AbortedResult, ImpliesResult, State, StuckResult if TYPE_CHECKING: from pathlib import Path @@ -234,3 +234,21 @@ def test_implies_surfaces_indeterminate(indeterminate: bool | None) -> None: # Then assert result.csubst is None assert result.indeterminate is indeterminate + + +def test_implies_aborted_treated_as_indeterminate() -> None: + # Given a backend whose implies aborts (kore-rpc `code: 6`, e.g. recover-mode's direct + # kore-implies call hitting "unknown constraints" the proxy would otherwise absorb) + kore_client = Mock() + kore_client.implies.side_effect = AbortedError(data='unknown constraints') + cts = CTermSymbolic(kore_client, Mock()) + cts.kast_to_kore = Mock(return_value=Mock()) # type: ignore[method-assign] + antecedent: CTerm = Mock(free_vars=frozenset()) + consequent: CTerm = Mock(free_vars=frozenset()) + + # When + result = cts.implies(antecedent, consequent) + + # Then the abort is surfaced as an indeterminate, not-subsumed result rather than crashing + assert result.csubst is None + assert result.indeterminate is True diff --git a/pyk/src/tests/unit/kore/test_client.py b/pyk/src/tests/unit/kore/test_client.py index ff9413477a..37f24e3a24 100644 --- a/pyk/src/tests/unit/kore/test_client.py +++ b/pyk/src/tests/unit/kore/test_client.py @@ -8,6 +8,7 @@ from pyk.kore.prelude import INT, SORT_GENERATED_TOP_CELL, int_dv from pyk.kore.rpc import ( + AbortedError, AbortedResult, DefaultError, ImplicationError, @@ -16,6 +17,7 @@ JsonRpcError, KoreClient, KoreClientError, + MultipleStatesError, ParseError, PatternError, SatResult, @@ -400,6 +402,18 @@ def test_add_module( SmtSolverError('Failed to decide predicate.', int_dv(0)), r'SMT solver error: Failed to decide predicate. Pattern: \dv{SortInt{}}("0")', ), + ( + 'aborted-error', + JsonRpcError(message='Aborted', code=6, data='unknown constraints'), + AbortedError(data='unknown constraints'), + 'Backend aborted: unknown constraints', + ), + ( + 'multiple-states-error', + JsonRpcError(message='Multiple states', code=7, data='more than one state'), + MultipleStatesError(data='more than one state'), + 'Multiple states: more than one state', + ), ( 'default-error', JsonRpcError(message='foo', code=100, data={'bar': 1, 'baz': [2, 3]}), From 90f5fea1c696d44eeaf55208025cecb08d7341c3 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 8 Jun 2026 20:43:28 +0000 Subject: [PATCH 18/26] tests/unit/{cterm/test_symbolic,kcfg/test_explore,test_proof}: trim #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 --- pyk/src/tests/unit/cterm/test_symbolic.py | 149 +--------------- pyk/src/tests/unit/kcfg/test_explore.py | 11 +- pyk/src/tests/unit/test_proof.py | 204 +--------------------- 3 files changed, 6 insertions(+), 358 deletions(-) diff --git a/pyk/src/tests/unit/cterm/test_symbolic.py b/pyk/src/tests/unit/cterm/test_symbolic.py index 4dac195178..c382b2cb18 100644 --- a/pyk/src/tests/unit/cterm/test_symbolic.py +++ b/pyk/src/tests/unit/cterm/test_symbolic.py @@ -1,34 +1,19 @@ from __future__ import annotations -import json from typing import TYPE_CHECKING -from unittest.mock import Mock, patch +from unittest.mock import Mock import pytest -from pyk.cterm.symbolic import HASKELL_LOGGING_ENTRIES, CTermSymbolic, cterm_symbolic +from pyk.cterm.symbolic import CTermSymbolic from pyk.kast.prelude.ml import mlTop from pyk.kore.prelude import int_dv from pyk.kore.rpc import AbortedError, AbortedResult, ImpliesResult, State, StuckResult if TYPE_CHECKING: - from pathlib import Path - from pyk.cterm import CTerm -def _mock_client_cts(response: object) -> tuple[Mock, CTermSymbolic]: - """Build a `CTermSymbolic` whose backend returns ``response`` and whose Kast<->Kore - conversions are stubbed, returning the backend `Mock` so a test can inspect call args. - """ - kore_client = Mock() - kore_client.execute.return_value = response - cts = CTermSymbolic(kore_client, Mock()) - cts.kast_to_kore = Mock(return_value=Mock()) # type: ignore[method-assign] - cts.kore_to_kast = Mock(return_value=mlTop()) # type: ignore[method-assign] - return kore_client, cts - - def _cterm_symbolic(response: object) -> CTermSymbolic: """Build a `CTermSymbolic` whose backend returns ``response`` and whose Kast<->Kore conversions are stubbed, so ``execute`` can be exercised without a real ``KDefinition``. @@ -43,109 +28,6 @@ def _cterm_symbolic(response: object) -> CTermSymbolic: return cts -def test_execute_on_requests_configured_entries() -> None: - # Given - kore_client, cts = _mock_client_cts(StuckResult(state=State(term=int_dv(2)), depth=1, logs=())) - dummy: CTerm = Mock() - - # When the per-call flag turns logging on - cts.execute(dummy, haskell_logging=True) - - # Then the configured entry set (the canonical default here) is what reaches KoreClient.execute - _args, kwargs = kore_client.execute.call_args - assert kwargs['haskell_logging'] == HASKELL_LOGGING_ENTRIES - - -def test_execute_honors_custom_entry_set() -> None: - # Given a CTermSymbolic configured with a custom entry set - kore_client = Mock() - kore_client.execute.return_value = StuckResult(state=State(term=int_dv(2)), depth=1, logs=()) - cts = CTermSymbolic(kore_client, Mock(), haskell_log_entries=['Rewrite', 'DebugApplyEquation']) - cts.kast_to_kore = Mock(return_value=Mock()) # type: ignore[method-assign] - cts.kore_to_kast = Mock(return_value=mlTop()) # type: ignore[method-assign] - - # When - cts.execute(Mock(), haskell_logging=True) - - # Then exactly that set is requested - _args, kwargs = kore_client.execute.call_args - assert kwargs['haskell_logging'] == ('Rewrite', 'DebugApplyEquation') - - -def test_execute_default_leaves_haskell_logging_off() -> None: - # Given - kore_client, cts = _mock_client_cts(StuckResult(state=State(term=int_dv(2)), depth=1, logs=())) - dummy: CTerm = Mock() - - # When called with defaults - cts.execute(dummy) - - # Then logging is left untouched (None preserves today's behaviour) - _args, kwargs = kore_client.execute.call_args - assert kwargs['haskell_logging'] is None - - -def _log_dir_cts(response: object, haskell_log_dir: Path) -> tuple[Mock, CTermSymbolic]: - kore_client = Mock() - kore_client.execute.return_value = response - cts = CTermSymbolic(kore_client, Mock(), haskell_log_dir=haskell_log_dir) - cts.kast_to_kore = Mock(return_value=Mock()) # type: ignore[method-assign] - cts.kore_to_kast = Mock(return_value=mlTop()) # type: ignore[method-assign] - return kore_client, cts - - -def test_execute_writes_haskell_log_bundle(tmp_path: Path) -> None: - # Given a configured log dir and a response carrying a per-request bundle - entry = {'context': ['Proxy'], 'message': 'simplifying'} - response = StuckResult(state=State(term=int_dv(2)), depth=1, logs=(), haskell_log_entries=(entry,)) - kore_client, cts = _log_dir_cts(response, tmp_path) - kore_client.last_request_id = 'proof-007' - - # When - cts.execute(Mock()) - - # Then logging is requested and the bundle lands in /.jsonl, one JSON value per line - _args, kwargs = kore_client.execute.call_args - assert kwargs['haskell_logging'] == HASKELL_LOGGING_ENTRIES - log_file = tmp_path / 'proof-007.jsonl' - assert json.loads(log_file.read_text().strip()) == entry - - -def test_execute_writes_no_file_when_bundle_absent(tmp_path: Path) -> None: - # Given a configured log dir but a response with no bundle - response = StuckResult(state=State(term=int_dv(2)), depth=1, logs=(), haskell_log_entries=None) - kore_client, cts = _log_dir_cts(response, tmp_path) - kore_client.last_request_id = 'proof-008' - - # When - cts.execute(Mock()) - - # Then nothing is written - assert not list(tmp_path.iterdir()) - - -def test_cterm_symbolic_forwards_custom_entry_set() -> None: - # Given a caller that overrides the per-request entry set through the factory - with patch('pyk.cterm.symbolic.KoreClient'): - with cterm_symbolic( - definition=Mock(), - definition_dir=Mock(), - start_server=False, - port=1, - haskell_log_entries=['Rewrite', 'DebugApplyEquation'], - ) as cts: - # Then the built CTermSymbolic requests exactly that set - assert cts._haskell_log_entries == ('Rewrite', 'DebugApplyEquation') - - -def test_cterm_symbolic_defaults_to_canonical_entry_set() -> None: - # Given no override - with patch('pyk.cterm.symbolic.KoreClient'): - with cterm_symbolic(definition=Mock(), definition_dir=Mock(), start_server=False, port=1) as cts: - # Then the canonical default is used - assert cts._haskell_log_entries == HASKELL_LOGGING_ENTRIES - - def test_execute_raises_on_abort_by_default() -> None: # Given cts = _cterm_symbolic(AbortedResult(state=State(term=int_dv(1)), depth=0, unknown_predicate=None, logs=())) @@ -183,33 +65,6 @@ def test_execute_not_aborted_on_normal_result() -> None: assert result.depth == 1 -def test_execute_forwards_per_call_params() -> None: - # Given - kore_client, cts = _mock_client_cts(StuckResult(state=State(term=int_dv(2)), depth=1, logs=())) - - # When - cts.execute(Mock(), booster_only_simplify=True, haskell_logging=True, raise_on_aborted=False) - - # Then the per-call flags reach the underlying KoreClient.execute; the haskell_logging bool is - # resolved to the configured entry set on the way through. - _args, kwargs = kore_client.execute.call_args - assert kwargs['booster_only_simplify'] is True - assert kwargs['haskell_logging'] == HASKELL_LOGGING_ENTRIES - - -def test_execute_default_params_preserve_current_call() -> None: - # Given - kore_client, cts = _mock_client_cts(StuckResult(state=State(term=int_dv(2)), depth=1, logs=())) - - # When called with defaults - cts.execute(Mock()) - - # Then booster-only falls back to the instance default (False) and logging is off - _args, kwargs = kore_client.execute.call_args - assert kwargs['booster_only_simplify'] is False - assert kwargs['haskell_logging'] is None - - @pytest.mark.parametrize('indeterminate', [True, False, None], ids=['true', 'false', 'absent']) def test_implies_surfaces_indeterminate(indeterminate: bool | None) -> None: # Given a falsifiable implication carrying the backend `indeterminate` flag diff --git a/pyk/src/tests/unit/kcfg/test_explore.py b/pyk/src/tests/unit/kcfg/test_explore.py index 64ca01b06c..61af75ee56 100644 --- a/pyk/src/tests/unit/kcfg/test_explore.py +++ b/pyk/src/tests/unit/kcfg/test_explore.py @@ -51,26 +51,22 @@ def test_extend_cterm_step_on_progress() -> None: ids=['booster', 'kore'], ) def test_simplify_variant_producer_and_capture(booster_only: bool, expected_producer: Producer) -> None: - # Given a cterm_symbolic that simplifies to a new term and exposes request id + log entries - entries = ({'context': ['proxy'], 'message': 'x'},) + # Given a cterm_symbolic that simplifies to a new term and exposes the request id cterm_symbolic = Mock() cterm_symbolic.simplify.return_value = (term(2), ()) cterm_symbolic.last_request_id = 'claim-001' - cterm_symbolic.last_haskell_log_entries = entries explore = KCFGExplore(cterm_symbolic) # When variant = explore.simplify_variant(term(1), booster_only=booster_only) - # Then the producer matches the backend, and request_id + entries are captured + # Then the producer matches the backend, and the request_id is captured assert variant.producer is expected_producer assert variant.cterm == term(2) assert variant.request_id == 'claim-001' - assert variant.log_entries == entries - # And the simplify was invoked with logging on and the right backend + # And the simplify was invoked with the right backend _args, kwargs = cterm_symbolic.simplify.call_args assert kwargs['booster_only_simplify'] is booster_only - assert kwargs['haskell_logging'] is True def test_simplify_variant_noop_still_yields_variant() -> None: @@ -78,7 +74,6 @@ def test_simplify_variant_noop_still_yields_variant() -> None: cterm_symbolic = Mock() cterm_symbolic.simplify.return_value = (term(1), ()) cterm_symbolic.last_request_id = 'claim-002' - cterm_symbolic.last_haskell_log_entries = None explore = KCFGExplore(cterm_symbolic) # When diff --git a/pyk/src/tests/unit/test_proof.py b/pyk/src/tests/unit/test_proof.py index 1d13fa7ae2..e508c1e6ab 100644 --- a/pyk/src/tests/unit/test_proof.py +++ b/pyk/src/tests/unit/test_proof.py @@ -1,6 +1,5 @@ from __future__ import annotations -import json from typing import TYPE_CHECKING from unittest.mock import Mock @@ -11,8 +10,7 @@ from pyk.kast.prelude.kbool import BOOL from pyk.kast.prelude.kint import intToken from pyk.kcfg.exploration import KCFGExplorationNodeAttr -from pyk.kcfg.explore import SimplifyVariant -from pyk.kcfg.kcfg import KCFG, KCFGNodeAttr, KoreHandoff, NodeVariant, NoProgress, Producer, Step +from pyk.kcfg.kcfg import KCFG, KCFGNodeAttr, KoreHandoff, NodeVariant, Producer, Step from pyk.proof import EqualityProof from pyk.proof.implies import EqualitySummary from pyk.proof.proof import CompositeSummary, Proof, ProofStatus @@ -24,12 +22,10 @@ APRProofRecoverCloseResult, APRProofRecoverNoProgressResult, APRProofStuckResult, - APRProofTerminalResult, APRProver, APRSummary, DecisiveInvalid, Indeterminate, - LoggedCall, RecoverTask, Subsumed, recover_task_for, @@ -371,148 +367,6 @@ def test_recover_task_noop_shortcircuit() -> None: assert recover_task_for(node) is RecoverTask.SIMPLIFY_KORE -# --- step_proof recover dispatch (C13) ----------------------------------------------------------- - - -def _recover_prover(*, node: KCFG.Node) -> Mock: - """A Mock APRProver wired enough to exercise the unbound `_recover_*` methods.""" - prover = Mock() - prover.optimize_kcfg = False - prover.cut_point_rules = [] - prover.terminal_rules = [] - prover.execute_depth = None - prover.kcfg_explore.kcfg_semantics.is_terminal.return_value = False - prover.kcfg_explore.cterm_symbolic.last_request_id = 'req-1' - prover.kcfg_explore.cterm_symbolic.last_haskell_log_entries = ({'message': 'log'},) - return prover - - -def _step(node: KCFG.Node, task: RecoverTask) -> Mock: - return Mock(node=node, target=node, proof_id='p', circularity=False, nonzero_depth=True, recover_task=task) - - -def test_recover_simplify_yields_add_variant() -> None: - node = KCFG.Node(1, term(1)) - prover = _recover_prover(node=node) - prover.kcfg_explore.simplify_variant.return_value = SimplifyVariant( - Producer.BOOSTER_SIMPLIFY, term(2), 'req-s', ({'message': 'log'},) - ) - - result = APRProver._recover_simplify(prover, _step(node, RecoverTask.SIMPLIFY_BOOSTER), (), booster_only=True) - - assert len(result) == 1 - variant_result = result[0] - assert isinstance(variant_result, APRProofAddVariantResult) - assert variant_result.producer is Producer.BOOSTER_SIMPLIFY - assert variant_result.cterm == term(2) - assert variant_result.request_id == 'req-s' - - -def test_recover_try_booster_close() -> None: - node = KCFG.Node(1, term(1)) - prover = _recover_prover(node=node) - prover._check_subsume.return_value = Subsumed(CSubst()) - - result = APRProver._recover_try(prover, _step(node, RecoverTask.TRY_BOOSTER), (), is_kore=False) - - assert isinstance(result[-1], APRProofRecoverCloseResult) - # booster close → no kore handoff - assert result[-1].kore_request_id is None - - -def test_recover_try_booster_advance() -> None: - node = KCFG.Node(1, term(1)) - prover = _recover_prover(node=node) - prover._check_subsume.return_value = DecisiveInvalid() - prover.kcfg_explore.extend_cterm.return_value = [Mock()] # not NoProgress ⇒ advance - - result = APRProver._recover_try(prover, _step(node, RecoverTask.TRY_BOOSTER), (), is_kore=False) - - assert isinstance(result[0], APRProofRecoverAdvanceResult) - assert result[0].kore_request_id is None - - -def test_recover_try_booster_no_progress_carries_indeterminate() -> None: - node = KCFG.Node(1, term(1)) - prover = _recover_prover(node=node) - prover._check_subsume.return_value = Indeterminate() - prover.kcfg_explore.extend_cterm.return_value = [NoProgress()] - - result = APRProver._recover_try(prover, _step(node, RecoverTask.TRY_BOOSTER), (), is_kore=False) - - no_progress = result[0] - assert isinstance(no_progress, APRProofRecoverNoProgressResult) - assert no_progress.backend == 'booster' - assert no_progress.subsume_indeterminate is True - - -def test_recover_try_kore_skips_implies_without_indeterminate_flag() -> None: - # rung-2 node without SUBSUME_INDETERMINATE: trust the decisive booster invalid, go to execute. - node = KCFG.Node(1, term(1), [KCFGNodeAttr.BOOSTER_TRIED]) - prover = _recover_prover(node=node) - prover.kcfg_explore.extend_cterm.return_value = [Mock()] - - result = APRProver._recover_try(prover, _step(node, RecoverTask.TRY_KORE), (), is_kore=True) - - prover._check_subsume.assert_not_called() - advance = result[0] - assert isinstance(advance, APRProofRecoverAdvanceResult) - # kore execute advance → handoff request id captured - assert advance.kore_request_id == 'req-1' - - -def test_recover_try_kore_close_records_handoff_id() -> None: - node = KCFG.Node(1, term(1), [KCFGNodeAttr.SUBSUME_INDETERMINATE]) - prover = _recover_prover(node=node) - prover._check_subsume.return_value = Subsumed(CSubst()) - - result = APRProver._recover_try(prover, _step(node, RecoverTask.TRY_KORE), (), is_kore=True) - - prover._check_subsume.assert_called_once() - close = result[-1] - assert isinstance(close, APRProofRecoverCloseResult) - assert close.kore_request_id == 'req-1' # kore implies closed ⇒ handoff id set - - -@pytest.mark.parametrize('subsumption', [Indeterminate(), DecisiveInvalid()], ids=['indeterminate', 'decisive-invalid']) -def test_recover_try_terminal_booster_escalates_instead_of_failing(subsumption: object) -> None: - # Regression (recover-mode parity): a terminal node whose booster subsumption does not close must - # NOT be finalized as terminal at the booster rung — that drops it out of `pending` before the - # ladder can reach a kore implies, regressing proofs that normal mode's kore-capable proxy implies - # would close. Both a booster `Indeterminate` and a decisive booster `invalid` escalate: for a - # terminal node we always want kore's second opinion before declaring it failing. - node = KCFG.Node(1, term(1)) - prover = _recover_prover(node=node) - prover.kcfg_explore.kcfg_semantics.is_terminal.return_value = True - prover._check_subsume.return_value = subsumption - - result = APRProver._recover_try(prover, _step(node, RecoverTask.TRY_BOOSTER), (), is_kore=False) - - # Not finalized as terminal; escalates so the node climbs to TRY_KORE's kore implies. - assert not any(isinstance(r, APRProofTerminalResult) for r in result) - no_progress = result[0] - assert isinstance(no_progress, APRProofRecoverNoProgressResult) - assert no_progress.backend == 'booster' - assert no_progress.subsume_indeterminate is True - prover.kcfg_explore.extend_cterm.assert_not_called() # a terminal node is never executed - - -def test_recover_try_terminal_kore_finalizes_when_implies_fails() -> None: - # The kore rung is the top of the ladder: once the kore implies on a terminal node also fails to - # close, the node is legitimately finalized as terminal (and so, unsubsumed, becomes failing). - node = KCFG.Node(1, term(1), [KCFGNodeAttr.SUBSUME_INDETERMINATE]) - prover = _recover_prover(node=node) - prover.kcfg_explore.kcfg_semantics.is_terminal.return_value = True - prover._check_subsume.return_value = DecisiveInvalid() - - result = APRProver._recover_try(prover, _step(node, RecoverTask.TRY_KORE), (), is_kore=True) - - prover._check_subsume.assert_called_once() - assert len(result) == 1 - assert isinstance(result[0], APRProofTerminalResult) - prover.kcfg_explore.extend_cterm.assert_not_called() - - # --- commit recover transitions (C14) ------------------------------------------------------------ @@ -532,7 +386,6 @@ def _no_progress(node_id: int, backend: str, indeterminate: bool = False) -> APR optimize_kcfg=False, backend=backend, subsume_indeterminate=indeterminate, - logged_calls=(), ) @@ -544,7 +397,6 @@ def _add_variant(node_id: int, producer: Producer, cterm: CTerm) -> APRProofAddV producer=producer, cterm=cterm, request_id='r', - log_entries=None, ) @@ -601,7 +453,6 @@ def test_commit_recover_close_records_implies_handoff() -> None: optimize_kcfg=False, csubst=CSubst(), kore_request_id='r-imp', - logged_calls=(), ) ) assert proof.kcfg.kore_handoffs == [ @@ -618,7 +469,6 @@ def test_commit_recover_advance_records_execute_handoff() -> None: optimize_kcfg=False, extension_to_apply=Step(term(50), 1, (), []), kore_request_id='r-exec', - logged_calls=(), ) ) handoffs = proof.kcfg.kore_handoffs @@ -638,63 +488,11 @@ def test_commit_recover_advance_no_handoff_for_booster() -> None: optimize_kcfg=False, extension_to_apply=Step(term(50), 1, (), []), kore_request_id=None, - logged_calls=(), ) ) assert proof.kcfg.kore_handoffs == [] -def test_commit_writes_recover_logs(proof_dir: Path) -> None: - kcfg = KCFG() - n_init = kcfg.create_node(term(1)) - n_target = kcfg.create_node(term(2)) - n = kcfg.create_node(term(3)) - proof = APRProof(id='rec', kcfg=kcfg, terminal=[], init=n_init.id, target=n_target.id, logs={}, proof_dir=proof_dir) - entries = ({'context': ['proxy'], 'message': 'x'}, {'rule_id': 'abc', 'pre_hash': 'd'}) - - proof.commit( - APRProofRecoverNoProgressResult( - node_id=n.id, - prior_loops_cache_update=(), - optimize_kcfg=False, - backend='kore', - subsume_indeterminate=False, - logged_calls=(LoggedCall('claim-007', entries),), - ) - ) - - assert proof.proof_subdir is not None - log_file = proof.proof_subdir / 'recover-logs' / 'claim-007.jsonl' - assert log_file.exists() - parsed = [json.loads(line) for line in log_file.read_text().splitlines()] - assert parsed == [dict(entry) for entry in entries] - - -def test_commit_recover_logs_skipped_when_no_entries(proof_dir: Path) -> None: - kcfg = KCFG() - n_init = kcfg.create_node(term(1)) - n_target = kcfg.create_node(term(2)) - n = kcfg.create_node(term(3)) - proof = APRProof( - id='rec2', kcfg=kcfg, terminal=[], init=n_init.id, target=n_target.id, logs={}, proof_dir=proof_dir - ) - - # A call that captured no entries (None) writes no file. - proof.commit( - APRProofRecoverNoProgressResult( - node_id=n.id, - prior_loops_cache_update=(), - optimize_kcfg=False, - backend='booster', - subsume_indeterminate=False, - logged_calls=(LoggedCall('claim-008', None),), - ) - ) - - assert proof.proof_subdir is not None - assert not (proof.proof_subdir / 'recover-logs' / 'claim-008.jsonl').exists() - - def test_apr_proof_minimization_and_terminals() -> None: # 25 /-- X >=Int 5 --> 10 # 5 10 15 20 /-- X >=Int 0 --> 6 --> 8 From d2b2011043905952475e386d0f641ea5e172e73b Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 8 Jun 2026 20:43:28 +0000 Subject: [PATCH 19/26] kore/rpc, cterm/symbolic, kcfg/explore, proof/reachability: drop recover-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 -> /.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 --- pyk/src/pyk/cterm/symbolic.py | 12 +++--- pyk/src/pyk/kcfg/explore.py | 21 +++++------ pyk/src/pyk/kore/rpc.py | 22 +---------- pyk/src/pyk/proof/reachability.py | 61 ++----------------------------- 4 files changed, 20 insertions(+), 96 deletions(-) diff --git a/pyk/src/pyk/cterm/symbolic.py b/pyk/src/pyk/cterm/symbolic.py index c62e97cbae..3bbe7ce1eb 100644 --- a/pyk/src/pyk/cterm/symbolic.py +++ b/pyk/src/pyk/cterm/symbolic.py @@ -158,13 +158,13 @@ def _capture_haskell_log(self, entries: tuple[Any, ...] | None) -> None: @property def last_request_id(self) -> str | None: - """JSON-RPC id of the most recent RPC issued on this thread (see `KoreClient.last_request_id`).""" - return self._kore_client.last_request_id + """JSON-RPC id of the most recent RPC issued by the backing client (see `KoreClient.last_request_id`). - @property - def last_haskell_log_entries(self) -> tuple[Any, ...] | None: - """`haskell-log-entries` bundle of the most recent RPC on this thread (see `KoreClient`).""" - return self._kore_client.last_haskell_log_entries + Recover-mode snapshots this immediately after a simplify to key the `KoreHandoff` to that + request, so a handoff can be correlated with the per-request log file that the configured + `haskell_log_dir` writer (see `_capture_haskell_log`) emits for the same id. + """ + return self._kore_client.last_request_id def execute( self, diff --git a/pyk/src/pyk/kcfg/explore.py b/pyk/src/pyk/kcfg/explore.py index 141c7b0f0e..15f2f493d2 100644 --- a/pyk/src/pyk/kcfg/explore.py +++ b/pyk/src/pyk/kcfg/explore.py @@ -22,7 +22,7 @@ if TYPE_CHECKING: from collections.abc import Iterable - from typing import Any, Final + from typing import Final from ..cterm import CTerm, CTermSymbolic from ..kast import KInner @@ -38,15 +38,15 @@ class SimplifyVariant(NamedTuple): """Result of a recover-mode variant-producing simplification. - Carries everything the coordinator needs to land the variant (`KCFG.add_variant`) and store its - captured logs (keyed by `request_id`): the `producer`, the simplified `cterm`, the simplify RPC's - `request_id`, and the `haskell-log-entries` bundle (`None` if the backend captured nothing). + Carries what the coordinator needs to land the variant (`KCFG.add_variant`) and key its + `KoreHandoff`: the `producer`, the simplified `cterm`, and the simplify RPC's `request_id`. + The per-request haskell log bundle, when wanted, is written by the configured `haskell_log_dir` + (see `CTermSymbolic._capture_haskell_log`) under the same `request_id`. """ producer: Producer cterm: CTerm request_id: str | None - log_entries: tuple[Any, ...] | None class KCFGExplore: @@ -151,22 +151,19 @@ def simplify(self, cfg: KCFG, logs: dict[int, tuple[LogEntry, ...]]) -> None: logs[node.id] = next_node_logs def simplify_variant(self, cterm: CTerm, *, booster_only: bool) -> SimplifyVariant: - """Re-simplify ``cterm`` with one backend, capturing the request id and per-request logs. + """Re-simplify ``cterm`` with one backend, capturing the request id of the call. Non-destructive: returns a `SimplifyVariant` for the coordinator to land via `KCFG.add_variant`; the recover-mode ladder uses `booster_only=True` (rung 0→1) then - `booster_only=False` (rung 1→2). Always logs (`haskell_logging=True`) — every simplify on - the ladder is diagnostic-relevant. + `booster_only=False` (rung 1→2). Per-request haskell logging is governed by the + `CTermSymbolic`'s configured `haskell_log_dir`, not forced here. """ producer = Producer.BOOSTER_SIMPLIFY if booster_only else Producer.KORE_SIMPLIFY - simplified, _logs = self.cterm_symbolic.simplify( - cterm, booster_only_simplify=booster_only, haskell_logging=True - ) + simplified, _logs = self.cterm_symbolic.simplify(cterm, booster_only_simplify=booster_only) return SimplifyVariant( producer=producer, cterm=simplified, request_id=self.cterm_symbolic.last_request_id, - log_entries=self.cterm_symbolic.last_haskell_log_entries, ) def step( diff --git a/pyk/src/pyk/kore/rpc.py b/pyk/src/pyk/kore/rpc.py index 408f74d12e..294e6723f2 100644 --- a/pyk/src/pyk/kore/rpc.py +++ b/pyk/src/pyk/kore/rpc.py @@ -14,7 +14,7 @@ from pathlib import Path from signal import SIGINT from subprocess import DEVNULL, PIPE, Popen -from threading import Thread, local +from threading import Thread from time import sleep from typing import ClassVar # noqa: TC003 from typing import TYPE_CHECKING, ContextManager, NamedTuple, TypedDict, final @@ -48,11 +48,6 @@ # `ContextVar` values are not propagated by `ThreadPoolExecutor`. client_label: ContextVar[str | None] = ContextVar('kore_rpc_client_label', default=None) -# Records the `haskell-log-entries` bundle (or None) of the most recent response on the calling -# thread. Snapshotted alongside `last_request_id` so a diagnostic worker can capture the per-request -# logs of the exact call it just made without threading them through every result type. -_last_haskell_log_entries: local = local() - class KoreExecLogFormat(Enum): STANDARD = 'standard' @@ -1057,24 +1052,11 @@ def last_request_id(self) -> str | None: """ return self._client.last_request_id - @property - def last_haskell_log_entries(self) -> tuple[Any, ...] | None: - """The ``haskell-log-entries`` bundle of the most recent response on the calling thread. - - ``None`` when the last request did not set ``haskell-logging`` (or before any request). - Snapshot alongside ``last_request_id`` to store the per-request logs of that exact call. - """ - return getattr(_last_haskell_log_entries, 'value', None) - def _request(self, method: str, **params: Any) -> dict[str, Any]: try: - result = self._client.request(method, **params) + return self._client.request(method, **params) except JsonRpcError as err: raise self._error(err) from err - # Capture the per-request log bundle (if any) on this thread for `last_haskell_log_entries`. - entries = result.get('haskell-log-entries') - _last_haskell_log_entries.value = tuple(entries) if entries is not None else None - return result def _error(self, err: JsonRpcError) -> KoreClientError: assert err.code not in {-32601, -32602}, 'Malformed Kore-RPC request' diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 83541f1464..5f05f6b4c0 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -127,14 +127,6 @@ class APRProofStuckResult(APRProofResult): """ -@dataclass(frozen=True) -class LoggedCall: - """One kore RPC whose captured per-request log bundle the coordinator writes to disk (§5).""" - - request_id: str - log_entries: tuple[Any, ...] | None - - @dataclass class APRProofAddVariantResult(APRProofResult): """Recover-mode: a re-simplification variant for `commit` to append via `KCFG.add_variant`.""" @@ -142,7 +134,6 @@ class APRProofAddVariantResult(APRProofResult): producer: Producer cterm: CTerm request_id: str | None - log_entries: tuple[Any, ...] | None @dataclass @@ -151,7 +142,6 @@ class APRProofRecoverNoProgressResult(APRProofResult): backend: str # 'booster' | 'kore' subsume_indeterminate: bool - logged_calls: tuple[LoggedCall, ...] @dataclass @@ -164,7 +154,6 @@ class APRProofRecoverAdvanceResult(APRProofResult): extension_to_apply: KCFGExtendResult kore_request_id: str | None - logged_calls: tuple[LoggedCall, ...] @dataclass @@ -177,7 +166,6 @@ class APRProofRecoverCloseResult(APRProofResult): csubst: CSubst kore_request_id: str | None - logged_calls: tuple[LoggedCall, ...] class SubsumptionCheck(ABC): @@ -407,7 +395,6 @@ def commit(self, result: APRProofResult) -> None: source=result.node_id, target=target_id, flavour='execute', request_id=result.kore_request_id ) ) - self._write_recover_logs(result.logged_calls) elif isinstance(result, APRProofRecoverCloseResult): self.kcfg.create_cover(result.node_id, self.target, csubst=result.csubst) if result.kore_request_id is not None: @@ -416,7 +403,6 @@ def commit(self, result: APRProofResult) -> None: source=result.node_id, target=self.target, flavour='implies', request_id=result.kore_request_id ) ) - self._write_recover_logs(result.logged_calls) elif isinstance(result, APRProofBoundedResult): self.add_bounded(result.node_id) else: @@ -432,8 +418,6 @@ def _commit_add_variant(self, result: APRProofAddVariantResult) -> None: if result.cterm != prev_cterm: self.kcfg.discard_attr(result.node_id, KCFGNodeAttr.BOOSTER_TRIED) self.kcfg.discard_attr(result.node_id, KCFGNodeAttr.SUBSUME_INDETERMINATE) - if result.request_id is not None and result.log_entries is not None: - self._write_recover_logs((LoggedCall(result.request_id, result.log_entries),)) def _commit_recover_no_progress(self, result: APRProofRecoverNoProgressResult) -> None: if result.backend == 'kore': @@ -450,7 +434,6 @@ def _commit_recover_no_progress(self, result: APRProofRecoverNoProgressResult) - self.kcfg.add_attr(result.node_id, KCFGNodeAttr.BOTH_BACKENDS_FAILED) _LOGGER.info(f'Both backends failed, stuck node {self.id}: {result.node_id}') self.kcfg.add_stuck(result.node_id) - self._write_recover_logs(result.logged_calls) def _recover_successor_id(self, node_id: int) -> int: """Resolve the kore execute handoff target: the (min) new successor of ``node_id``. @@ -463,24 +446,6 @@ def _recover_successor_id(self, node_id: int) -> int: targets = [target_id for succ in self.kcfg.successors(node_id) for target_id in succ.target_ids] return min(targets) if targets else node_id - def _write_recover_logs(self, logged_calls: Iterable[LoggedCall]) -> None: - """Write one ``recover-logs/{request_id}.jsonl`` per logged kore call (§5). - - Each line is one captured log entry in ``--log-format json`` shape, so the file feeds - straight into ``parse_kore_log``. No-ops when the proof is in-memory (no ``proof_subdir``) - or a call captured no entries. Disk writes stay on the coordinator (main) thread. - """ - if self.proof_subdir is None: - return - log_dir = self.proof_subdir / 'recover-logs' - for call in logged_calls: - if call.log_entries is None: - continue - ensure_dir_path(log_dir) - (log_dir / f'{call.request_id}.jsonl').write_text( - '\n'.join(json.dumps(entry) for entry in call.log_entries) - ) - def nonzero_depth(self, node: KCFG.Node) -> bool: return not self.kcfg.zero_depth_between(self.init, node.id) @@ -1047,7 +1012,6 @@ def _check_subsume( target_node: KCFG.Node, proof_id: str, booster_only: bool | None = None, - haskell_logging: bool | None = None, ) -> SubsumptionCheck: target_cterm = target_node.cterm _LOGGER.debug(f'Checking subsumption into target state {proof_id}: {shorten_hashes((node.id, target_cterm))}') @@ -1059,7 +1023,6 @@ def _check_subsume( target_cterm, assume_defined=self.assume_defined, booster_only_simplify=booster_only, - haskell_logging=haskell_logging, ) if result.csubst is not None: _LOGGER.info(f'Subsumed into target node {proof_id}: {shorten_hashes((node.id, target_node.id))}') @@ -1213,7 +1176,6 @@ def _recover_simplify( producer=variant.producer, cterm=variant.cterm, request_id=variant.request_id, - log_entries=variant.log_entries, ) ] @@ -1221,16 +1183,6 @@ def _recover_try(self, step: APRProofStep, prior_loops: tuple[int, ...], *, is_k node = step.node cs = self.kcfg_explore.cterm_symbolic semantics = self.kcfg_explore.kcfg_semantics - # §3e: rung-0 booster tries (the happy path) are not logged; everything else is. - should_log = is_kore or recovery_rung(node) >= 1 - logged_calls: list[LoggedCall] = [] - - def capture() -> str | None: - rid = cs.last_request_id - if should_log and rid is not None: - logged_calls.append(LoggedCall(rid, cs.last_haskell_log_entries)) - return rid - is_terminal = semantics.is_terminal(node.cterm) target_is_terminal = semantics.is_terminal(step.target.cterm) terminal_result: list[APRProofResult] = ( @@ -1251,10 +1203,8 @@ def capture() -> str | None: not is_kore or KCFGNodeAttr.SUBSUME_INDETERMINATE in node.attrs ) if run_subsume: - subsumption = self._check_subsume( - node, step.target, proof_id=step.proof_id, booster_only=not is_kore, haskell_logging=should_log - ) - request_id = capture() + subsumption = self._check_subsume(node, step.target, proof_id=step.proof_id, booster_only=not is_kore) + request_id = cs.last_request_id if isinstance(subsumption, Subsumed): return terminal_result + [ APRProofRecoverCloseResult( @@ -1263,7 +1213,6 @@ def capture() -> str | None: optimize_kcfg=self.optimize_kcfg, csubst=subsumption.csubst, kore_request_id=request_id if is_kore else None, - logged_calls=tuple(logged_calls), ) ] subsume_indeterminate = isinstance(subsumption, Indeterminate) @@ -1288,7 +1237,6 @@ def capture() -> str | None: optimize_kcfg=self.optimize_kcfg, backend='booster', subsume_indeterminate=True, - logged_calls=tuple(logged_calls), ) ] return terminal_result @@ -1310,9 +1258,8 @@ def capture() -> str | None: node_id=node.id, booster_only_simplify=not is_kore, raise_on_aborted=False, - haskell_logging=should_log, ) - request_id = capture() + request_id = cs.last_request_id # No progress: the worker does not stuck the node; commit sets the per-backend attr (C14). if extend_results and isinstance(extend_results[0], NoProgress): @@ -1323,7 +1270,6 @@ def capture() -> str | None: optimize_kcfg=self.optimize_kcfg, backend='kore' if is_kore else 'booster', subsume_indeterminate=subsume_indeterminate, - logged_calls=tuple(logged_calls), ) ] # Progress: apply the first extension (extend-and-cache is disabled in recover-mode). @@ -1334,7 +1280,6 @@ def capture() -> str | None: optimize_kcfg=self.optimize_kcfg, extension_to_apply=extend_results[0], kore_request_id=request_id if is_kore else None, - logged_calls=tuple(logged_calls), ) ] From 94a3c4f291ba24a1025a92c291508adbd2b702bb Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 8 Jun 2026 20:50:05 +0000 Subject: [PATCH 20/26] kcfg/kcfg, proof/reachability, kcfg/explore: enum-ize handoff flavour and recover backend, exhaustive task/backend matches, drop dangling design-doc refs MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- pyk/src/pyk/kcfg/explore.py | 2 +- pyk/src/pyk/kcfg/kcfg.py | 27 +++++-- pyk/src/pyk/proof/reachability.py | 82 +++++++++++++-------- pyk/src/tests/integration/proof/test_imp.py | 3 +- pyk/src/tests/unit/kcfg/test_store.py | 8 +- pyk/src/tests/unit/test_kcfg.py | 6 +- pyk/src/tests/unit/test_proof.py | 17 +++-- 7 files changed, 91 insertions(+), 54 deletions(-) diff --git a/pyk/src/pyk/kcfg/explore.py b/pyk/src/pyk/kcfg/explore.py index 15f2f493d2..549f833e43 100644 --- a/pyk/src/pyk/kcfg/explore.py +++ b/pyk/src/pyk/kcfg/explore.py @@ -285,7 +285,7 @@ def extend_cterm( # No-progress or vacuous. `Vacuous` is a context-free semantic verdict and stays here; a # depth-0 no-progress result is reported as the neutral `NoProgress` rather than `Stuck`, so - # the coordinator (`APRProof.commit`) decides whether the node is terminal (see C6). + # the coordinator (`APRProof.commit`) decides whether the node is terminal. if not next_states: if vacuous: extend_results.append(Vacuous()) diff --git a/pyk/src/pyk/kcfg/kcfg.py b/pyk/src/pyk/kcfg/kcfg.py index 4a828ef002..9d02a2ce8a 100644 --- a/pyk/src/pyk/kcfg/kcfg.py +++ b/pyk/src/pyk/kcfg/kcfg.py @@ -90,27 +90,40 @@ def from_dict(dct: dict[str, Any]) -> NodeVariant: return NodeVariant(Producer(dct['producer']), dct.get('request_id'), CTerm.from_dict(dct['cterm'])) +class HandoffFlavour(Enum): + """Which kore operation performed a `KoreHandoff` — an execute step or an implies (subsumption).""" + + EXECUTE = 'execute' + IMPLIES = 'implies' + + @final @dataclass(frozen=True) class KoreHandoff: """Record an operation-level kore handoff (execute or implies) where kore advanced the proof. Lets the diagnostic find every kore handoff without scanning logs. ``request_id`` is the join - key onto the stored per-request log (Layer 5). For ``execute``, ``source``/``target`` are the - lhs/rhs node ids; for ``implies``, ``source`` is the node and ``target`` the subsumption target. + key onto the per-request log file the configured ``haskell_log_dir`` writes for that request. + For ``execute``, ``source``/``target`` are the lhs/rhs node ids; for ``implies``, ``source`` is + the node and ``target`` the subsumption target. """ source: int target: int - flavour: str # 'execute' | 'implies' + flavour: HandoffFlavour request_id: str def to_dict(self) -> dict[str, Any]: - return {'source': self.source, 'target': self.target, 'flavour': self.flavour, 'request_id': self.request_id} + return { + 'source': self.source, + 'target': self.target, + 'flavour': self.flavour.value, + 'request_id': self.request_id, + } @staticmethod def from_dict(dct: dict[str, Any]) -> KoreHandoff: - return KoreHandoff(dct['source'], dct['target'], dct['flavour'], dct['request_id']) + return KoreHandoff(dct['source'], dct['target'], HandoffFlavour(dct['flavour']), dct['request_id']) class KCFGStore: @@ -118,7 +131,7 @@ class KCFGStore: # Node attributes persisted as top-level side-lists in `kcfg.json` (node files only carry # `cterm`/`variants`; `read_cfg_data` rebuilds `attrs` from these). Keep this the single source - # of truth so adding a persisted attr is a one-line change (see C10). + # of truth so adding a persisted attr is a one-line change. _ATTR_SIDE_LISTS: Final = { 'vacuous': KCFGNodeAttr.VACUOUS, 'stuck': KCFGNodeAttr.STUCK, @@ -191,7 +204,7 @@ class Node: # Simplification-provenance chain, least→most simplified, canonical term last; `()` == no # recorded history (back-compat default). `compare=False` excludes it from the dataclass's # generated eq/order/hash, so node identity is unchanged — `cterm` already reflects the - # canonical term, and the rest of the system stays oblivious to `variants` (see C8). + # canonical term, and the rest of the system stays oblivious to `variants`. variants: tuple[NodeVariant, ...] = field(default=(), compare=False) def __init__( diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 5f05f6b4c0..ce0572be67 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -15,7 +15,7 @@ from ..kast.prelude.ml import mlAnd, mlTop from ..kcfg import KCFG, KCFGStore from ..kcfg.exploration import KCFGExploration -from ..kcfg.kcfg import KCFGNodeAttr, KoreHandoff, NoProgress, Producer +from ..kcfg.kcfg import HandoffFlavour, KCFGNodeAttr, KoreHandoff, NoProgress, Producer from ..kore.rpc import LogEntry, client_label from ..ktool.claim_index import ClaimIndex from ..utils import FrozenDict, ensure_dir_path, hash_str, shorten_hashes, single @@ -39,7 +39,7 @@ class RecoverTask(Enum): - """The per-node task the recover-mode coordinator assigns to a worker (see §unifying model). + """The per-node task the recover-mode coordinator assigns to a worker. `TRY_BOOSTER`/`TRY_KORE` are the combined subsume-then-execute step with one backend; `SIMPLIFY_BOOSTER`/`SIMPLIFY_KORE` each produce one re-simplification variant. @@ -51,6 +51,13 @@ class RecoverTask(Enum): TRY_KORE = 'try-kore' +class RecoverBackend(Enum): + """Which backend a recover-mode `try` used — booster-only, or kore-enabled.""" + + BOOSTER = 'booster' + KORE = 'kore' + + def recovery_rung(node: KCFG.Node) -> int: """Compute the node's recovery rung: 0 (original), 1 (booster-simplified), 2 (kore-simplified). @@ -62,7 +69,7 @@ def recovery_rung(node: KCFG.Node) -> int: def recover_task_for(node: KCFG.Node) -> RecoverTask: - """Pick the next recover-mode task for a *pending* node from its rung and attrs (§3d). + """Pick the next recover-mode task for a *pending* node from its rung and attrs. A pending node never has both `BOOSTER_TRIED` and `KORE_TRIED` at rung 2 — `commit` would have marked that node stuck — so the rung-2 branch is always `TRY_KORE`. @@ -123,7 +130,7 @@ class APRProofStuckResult(APRProofResult): """The backend reported no progress; the coordinator (`commit`) is to mark the node stuck. Carrying this as a distinct result — rather than a `Stuck` extension applied by `KCFG.extend` — - keeps `add_stuck` solely in `commit`, where the full node context lives (see C6). + keeps `add_stuck` solely in `commit`, where the full node context lives. """ @@ -140,7 +147,7 @@ class APRProofAddVariantResult(APRProofResult): class APRProofRecoverNoProgressResult(APRProofResult): """Recover-mode: a `try` made no progress; `commit` sets the per-backend attr (and may stuck).""" - backend: str # 'booster' | 'kore' + backend: RecoverBackend subsume_indeterminate: bool @@ -173,7 +180,7 @@ class SubsumptionCheck(ABC): Distinguishes a decisive non-subsumption (``DecisiveInvalid`` — trust it) from a couldn't-determine (``Indeterminate`` — recover-mode escalates to a kore implies). Today both - map to "proceed to execute", identical to the old ``csubst is None`` (see C7). + map to "proceed to execute", identical to the old ``csubst is None``. """ @@ -321,7 +328,7 @@ def get_steps(self) -> list[APRProofStep]: ) # Recover-mode: the coordinator picks the per-node task and disables extend-and-cache - # (caching a second extend interacts badly with re-trying a node across rungs, §3b). + # (caching a second extend interacts badly with re-trying a node across rungs). recover_task = recover_task_for(node) if self.recover_mode else None use_cache = ( None @@ -374,7 +381,7 @@ def commit(self, result: APRProofResult) -> None: elif isinstance(result, APRProofTerminalResult): self.add_terminal(result.node_id) elif isinstance(result, APRProofStuckResult): - # Sole site that marks a node stuck: the coordinator owns this judgment (C6). + # Sole site that marks a node stuck: the coordinator owns this judgment. _LOGGER.info(f'Stuck node {self.id}: {result.node_id}') self.kcfg.add_stuck(result.node_id) elif isinstance(result, APRProofAddVariantResult): @@ -392,7 +399,10 @@ def commit(self, result: APRProofResult) -> None: target_id = self._recover_successor_id(result.node_id) self.kcfg.add_kore_handoff( KoreHandoff( - source=result.node_id, target=target_id, flavour='execute', request_id=result.kore_request_id + source=result.node_id, + target=target_id, + flavour=HandoffFlavour.EXECUTE, + request_id=result.kore_request_id, ) ) elif isinstance(result, APRProofRecoverCloseResult): @@ -400,7 +410,10 @@ def commit(self, result: APRProofResult) -> None: if result.kore_request_id is not None: self.kcfg.add_kore_handoff( KoreHandoff( - source=result.node_id, target=self.target, flavour='implies', request_id=result.kore_request_id + source=result.node_id, + target=self.target, + flavour=HandoffFlavour.IMPLIES, + request_id=result.kore_request_id, ) ) elif isinstance(result, APRProofBoundedResult): @@ -409,10 +422,10 @@ def commit(self, result: APRProofResult) -> None: raise ValueError(f'Incorrect result type, expected APRProofResult: {result}') def _commit_add_variant(self, result: APRProofAddVariantResult) -> None: - # Clear-iff-changed invariant (§3d): clear the per-rung try attrs only when the simplify - # actually changed the term, so the simplified node is re-tried with booster. A no-op - # variant leaves BOOSTER_TRIED set, so the next task is the next simplify rung (the no-op - # short-circuit) rather than a futile TRY_BOOSTER on the byte-identical term. + # Clear-iff-changed invariant: clear the per-rung try attrs only when the simplify actually + # changed the term, so the simplified node is re-tried with booster. A no-op variant leaves + # BOOSTER_TRIED set, so the next task is the next simplify rung (the no-op short-circuit) + # rather than a futile TRY_BOOSTER on the byte-identical term. prev_cterm = self.kcfg.node(result.node_id).cterm self.kcfg.add_variant(result.node_id, result.producer, result.cterm, result.request_id) if result.cterm != prev_cterm: @@ -420,14 +433,15 @@ def _commit_add_variant(self, result: APRProofAddVariantResult) -> None: self.kcfg.discard_attr(result.node_id, KCFGNodeAttr.SUBSUME_INDETERMINATE) def _commit_recover_no_progress(self, result: APRProofRecoverNoProgressResult) -> None: - if result.backend == 'kore': - self.kcfg.add_attr(result.node_id, KCFGNodeAttr.KORE_TRIED) - else: - self.kcfg.add_attr(result.node_id, KCFGNodeAttr.BOOSTER_TRIED) - if result.subsume_indeterminate: - self.kcfg.add_attr(result.node_id, KCFGNodeAttr.SUBSUME_INDETERMINATE) + match result.backend: + case RecoverBackend.KORE: + self.kcfg.add_attr(result.node_id, KCFGNodeAttr.KORE_TRIED) + case RecoverBackend.BOOSTER: + self.kcfg.add_attr(result.node_id, KCFGNodeAttr.BOOSTER_TRIED) + if result.subsume_indeterminate: + self.kcfg.add_attr(result.node_id, KCFGNodeAttr.SUBSUME_INDETERMINATE) # Rung-2 exhaustion: booster simplify, kore simplify, booster try, and kore try all failed to - # advance the node — a genuine dead-end. The coordinator (and only it) marks it stuck (C6), + # advance the node — a genuine dead-end. The coordinator (and only it) marks it stuck, # tagged so the diagnostic can distinguish it from an ordinary stuck. attrs = self.kcfg.node(result.node_id).attrs if KCFGNodeAttr.BOOSTER_TRIED in attrs and KCFGNodeAttr.KORE_TRIED in attrs: @@ -1028,7 +1042,7 @@ def _check_subsume( _LOGGER.info(f'Subsumed into target node {proof_id}: {shorten_hashes((node.id, target_node.id))}') return Subsumed(result.csubst) # Not subsumed: a decisive invalid is trusted; a couldn't-determine (booster - # `MatchIndeterminate`) is surfaced so recover-mode can escalate to a kore implies (C13). + # `MatchIndeterminate`) is surfaced so recover-mode can escalate to a kore implies. return Indeterminate() if result.indeterminate else DecisiveInvalid() def step_proof(self, step: APRProofStep) -> list[APRProofResult]: @@ -1051,7 +1065,7 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: ] # Recover-mode dispatches to a self-contained ladder step (terminal/subsume/execute are - # handled within, per the assigned task); the normal path below is left untouched (C13). + # handled within, per the assigned task); the normal path below is left untouched. if step.recover_task is not None: return self._recover_step(step, prior_loops) @@ -1123,7 +1137,7 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: # We can obtain two results at most assert len(extend_results) <= 2 # A no-progress result is not applied to the KCFG by the worker; the coordinator decides - # the node is stuck (sole `add_stuck` site is `commit`, see C6). + # the node is stuck (sole `add_stuck` site is `commit`). if len(extend_results) == 1 and isinstance(extend_results[0], NoProgress): return [ APRProofStuckResult( @@ -1160,9 +1174,15 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: def _recover_step(self, step: APRProofStep, prior_loops: tuple[int, ...]) -> list[APRProofResult]: task = step.recover_task assert task is not None - if task in (RecoverTask.SIMPLIFY_BOOSTER, RecoverTask.SIMPLIFY_KORE): - return self._recover_simplify(step, prior_loops, booster_only=task is RecoverTask.SIMPLIFY_BOOSTER) - return self._recover_try(step, prior_loops, is_kore=task is RecoverTask.TRY_KORE) + match task: + case RecoverTask.SIMPLIFY_BOOSTER: + return self._recover_simplify(step, prior_loops, booster_only=True) + case RecoverTask.SIMPLIFY_KORE: + return self._recover_simplify(step, prior_loops, booster_only=False) + case RecoverTask.TRY_BOOSTER: + return self._recover_try(step, prior_loops, is_kore=False) + case RecoverTask.TRY_KORE: + return self._recover_try(step, prior_loops, is_kore=True) def _recover_simplify( self, step: APRProofStep, prior_loops: tuple[int, ...], *, booster_only: bool @@ -1197,7 +1217,7 @@ def _recover_try(self, step: APRProofStep, prior_loops: tuple[int, ...], *, is_k # Subsumption: TRY_BOOSTER always checks (booster-only); TRY_KORE checks (kore) only when the # prior booster subsumption was indeterminate — otherwise we trust the decisive booster - # invalid and skip straight to kore-execute (§3b/§3c). + # invalid and skip straight to kore-execute. subsume_indeterminate = False run_subsume = (is_terminal == target_is_terminal) and ( not is_kore or KCFGNodeAttr.SUBSUME_INDETERMINATE in node.attrs @@ -1235,7 +1255,7 @@ def _recover_try(self, step: APRProofStep, prior_loops: tuple[int, ...], *, is_k node_id=node.id, prior_loops_cache_update=prior_loops, optimize_kcfg=self.optimize_kcfg, - backend='booster', + backend=RecoverBackend.BOOSTER, subsume_indeterminate=True, ) ] @@ -1261,14 +1281,14 @@ def _recover_try(self, step: APRProofStep, prior_loops: tuple[int, ...], *, is_k ) request_id = cs.last_request_id - # No progress: the worker does not stuck the node; commit sets the per-backend attr (C14). + # No progress: the worker does not stuck the node; commit sets the per-backend attr. if extend_results and isinstance(extend_results[0], NoProgress): return [ APRProofRecoverNoProgressResult( node_id=node.id, prior_loops_cache_update=prior_loops, optimize_kcfg=self.optimize_kcfg, - backend='kore' if is_kore else 'booster', + backend=RecoverBackend.KORE if is_kore else RecoverBackend.BOOSTER, subsume_indeterminate=subsume_indeterminate, ) ] diff --git a/pyk/src/tests/integration/proof/test_imp.py b/pyk/src/tests/integration/proof/test_imp.py index 7899151159..4df796caf3 100644 --- a/pyk/src/tests/integration/proof/test_imp.py +++ b/pyk/src/tests/integration/proof/test_imp.py @@ -15,6 +15,7 @@ from pyk.kast.prelude.kint import intToken from pyk.kast.prelude.ml import mlAnd, mlBottom, mlEquals, mlEqualsFalse, mlEqualsTrue, mlTop from pyk.kast.pretty import PrettyPrinter +from pyk.kcfg.kcfg import HandoffFlavour from pyk.kcfg.semantics import DefaultSemantics from pyk.kcfg.show import KCFGShow from pyk.proof import APRProver, ProofStatus @@ -931,7 +932,7 @@ def test_booster_recover_mode_prove( # Every recorded handoff/variant must name a Kore-producer with a request-id join key; a # node's canonical term always matches its variant chain's tail (invariant of add_variant). for handoff in proof.kcfg.kore_handoffs: - assert handoff.flavour in ('execute', 'implies') + assert handoff.flavour in (HandoffFlavour.EXECUTE, HandoffFlavour.IMPLIES) assert handoff.request_id for node in proof.kcfg.nodes: if node.variants: diff --git a/pyk/src/tests/unit/kcfg/test_store.py b/pyk/src/tests/unit/kcfg/test_store.py index a4e8992973..4e3e3aa803 100644 --- a/pyk/src/tests/unit/kcfg/test_store.py +++ b/pyk/src/tests/unit/kcfg/test_store.py @@ -9,7 +9,7 @@ from pyk.cterm import CTerm from pyk.kast.inner import KApply, KSequence from pyk.kast.prelude.utils import token -from pyk.kcfg.kcfg import KCFG, KCFGNodeAttr, KoreHandoff, Producer +from pyk.kcfg.kcfg import KCFG, HandoffFlavour, KCFGNodeAttr, KoreHandoff, Producer from pyk.kcfg.store import OptimizedNodeStore, _Cache from ..utils import a, b, c, f @@ -99,7 +99,7 @@ def test_kcfg_store_roundtrip_preserves_attrs_variants_handoffs(tmp_path: Path) cfg.add_attr(n2.id, KCFGNodeAttr.STUCK) cfg.add_attr(n2.id, KCFGNodeAttr.BOTH_BACKENDS_FAILED) cfg.add_variant(n1.id, Producer.BOOSTER_SIMPLIFY, _cell(3), request_id='r-1') - cfg.add_kore_handoff(KoreHandoff(source=n1.id, target=n2.id, flavour='execute', request_id='r-2')) + cfg.add_kore_handoff(KoreHandoff(source=n1.id, target=n2.id, flavour=HandoffFlavour.EXECUTE, request_id='r-2')) # When written and read back through KCFGStore cfg.write_cfg_data() @@ -114,7 +114,9 @@ def test_kcfg_store_roundtrip_preserves_attrs_variants_handoffs(tmp_path: Path) rn2 = restored.node(n2.id) assert KCFGNodeAttr.STUCK in rn2.attrs assert KCFGNodeAttr.BOTH_BACKENDS_FAILED in rn2.attrs - assert restored.kore_handoffs == [KoreHandoff(source=n1.id, target=n2.id, flavour='execute', request_id='r-2')] + assert restored.kore_handoffs == [ + KoreHandoff(source=n1.id, target=n2.id, flavour=HandoffFlavour.EXECUTE, request_id='r-2') + ] def test_kcfg_store_loads_legacy_without_new_keys(tmp_path: Path) -> None: diff --git a/pyk/src/tests/unit/test_kcfg.py b/pyk/src/tests/unit/test_kcfg.py index 2a044cd648..0cecea82e0 100644 --- a/pyk/src/tests/unit/test_kcfg.py +++ b/pyk/src/tests/unit/test_kcfg.py @@ -322,13 +322,13 @@ def test_node_equality_ignores_variants() -> None: def test_kore_handoffs_add_and_roundtrip() -> None: - from pyk.kcfg.kcfg import KoreHandoff + from pyk.kcfg.kcfg import HandoffFlavour, KoreHandoff # Given a kcfg with two recorded handoffs cfg = KCFG() cfg.create_node(term(1)) - cfg.add_kore_handoff(KoreHandoff(source=1, target=2, flavour='execute', request_id='claim-003')) - cfg.add_kore_handoff(KoreHandoff(source=2, target=2, flavour='implies', request_id='claim-004')) + cfg.add_kore_handoff(KoreHandoff(source=1, target=2, flavour=HandoffFlavour.EXECUTE, request_id='claim-003')) + cfg.add_kore_handoff(KoreHandoff(source=2, target=2, flavour=HandoffFlavour.IMPLIES, request_id='claim-004')) # Then the accessor returns them and they round-trip through to_dict/from_dict assert len(cfg.kore_handoffs) == 2 diff --git a/pyk/src/tests/unit/test_proof.py b/pyk/src/tests/unit/test_proof.py index e508c1e6ab..556b01a49e 100644 --- a/pyk/src/tests/unit/test_proof.py +++ b/pyk/src/tests/unit/test_proof.py @@ -10,7 +10,7 @@ from pyk.kast.prelude.kbool import BOOL from pyk.kast.prelude.kint import intToken from pyk.kcfg.exploration import KCFGExplorationNodeAttr -from pyk.kcfg.kcfg import KCFG, KCFGNodeAttr, KoreHandoff, NodeVariant, Producer, Step +from pyk.kcfg.kcfg import KCFG, HandoffFlavour, KCFGNodeAttr, KoreHandoff, NodeVariant, Producer, Step from pyk.proof import EqualityProof from pyk.proof.implies import EqualitySummary from pyk.proof.proof import CompositeSummary, Proof, ProofStatus @@ -26,6 +26,7 @@ APRSummary, DecisiveInvalid, Indeterminate, + RecoverBackend, RecoverTask, Subsumed, recover_task_for, @@ -273,7 +274,7 @@ def test_commit_stuck_result_marks_node_stuck() -> None: # When the coordinator commits a no-progress (stuck) result for that node proof.commit(APRProofStuckResult(node_id=n3.id, prior_loops_cache_update=(), optimize_kcfg=False)) - # Then the node is marked stuck — `commit` is the sole `add_stuck` site (C6) + # Then the node is marked stuck — `commit` is the sole `add_stuck` site assert kcfg.is_stuck(n3.id) @@ -307,7 +308,7 @@ def test_check_subsume_classification( # When (call the unbound method with the Mock as self) result = APRProver._check_subsume(prover, Mock(id=1), Mock(id=2), proof_id='p') - # Then the verdict is classified per §1c + # Then the verdict is classified assert isinstance(result, expected) if isinstance(result, Subsumed): assert result.csubst is csubst @@ -344,7 +345,7 @@ def test_recovery_rung() -> None: _TASK_DATA: tuple[tuple[str, int, list[NodeAttr], RecoverTask], ...] = ( - # (rung, attrs, expected) — first matching §3d rule + # (rung, attrs, expected) — first matching recover_task_for rule ('rung0-fresh', 0, [], RecoverTask.TRY_BOOSTER), ('rung0-tried', 0, [KCFGNodeAttr.BOOSTER_TRIED], RecoverTask.SIMPLIFY_BOOSTER), ('rung1-fresh', 1, [], RecoverTask.TRY_BOOSTER), @@ -367,7 +368,7 @@ def test_recover_task_noop_shortcircuit() -> None: assert recover_task_for(node) is RecoverTask.SIMPLIFY_KORE -# --- commit recover transitions (C14) ------------------------------------------------------------ +# --- commit recover transitions ------------------------------------------------------------------ def _recover_proof() -> tuple[APRProof, int]: @@ -384,7 +385,7 @@ def _no_progress(node_id: int, backend: str, indeterminate: bool = False) -> APR node_id=node_id, prior_loops_cache_update=(), optimize_kcfg=False, - backend=backend, + backend=RecoverBackend(backend), subsume_indeterminate=indeterminate, ) @@ -456,7 +457,7 @@ def test_commit_recover_close_records_implies_handoff() -> None: ) ) assert proof.kcfg.kore_handoffs == [ - KoreHandoff(source=nid, target=proof.target, flavour='implies', request_id='r-imp') + KoreHandoff(source=nid, target=proof.target, flavour=HandoffFlavour.IMPLIES, request_id='r-imp') ] @@ -473,7 +474,7 @@ def test_commit_recover_advance_records_execute_handoff() -> None: ) handoffs = proof.kcfg.kore_handoffs assert len(handoffs) == 1 - assert handoffs[0].flavour == 'execute' + assert handoffs[0].flavour == HandoffFlavour.EXECUTE assert handoffs[0].source == nid assert handoffs[0].request_id == 'r-exec' From 4877886d14f07058694437687c1e69bd783c0269 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 8 Jun 2026 21:11:48 +0000 Subject: [PATCH 21/26] tests/unit/{test_proof,kcfg/test_explore,cterm/test_symbolic,test_kcfg}: drop in-flux orchestration tests, parameterize and consolidate the rest MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- pyk/src/tests/unit/cterm/test_symbolic.py | 37 +++-- pyk/src/tests/unit/kcfg/test_explore.py | 84 +++--------- pyk/src/tests/unit/test_kcfg.py | 86 +++++------- pyk/src/tests/unit/test_proof.py | 158 ++-------------------- 4 files changed, 83 insertions(+), 282 deletions(-) diff --git a/pyk/src/tests/unit/cterm/test_symbolic.py b/pyk/src/tests/unit/cterm/test_symbolic.py index c382b2cb18..61d284e6a4 100644 --- a/pyk/src/tests/unit/cterm/test_symbolic.py +++ b/pyk/src/tests/unit/cterm/test_symbolic.py @@ -38,31 +38,26 @@ def test_execute_raises_on_abort_by_default() -> None: cts.execute(dummy) -def test_execute_surfaces_abort_when_not_raising() -> None: - # Given - cts = _cterm_symbolic(AbortedResult(state=State(term=int_dv(1)), depth=3, unknown_predicate=None, logs=())) - dummy: CTerm = Mock() - - # When - result = cts.execute(dummy, raise_on_aborted=False) - - # Then - assert result.aborted - assert result.depth == 3 - assert not result.vacuous +_ABORT_SURFACE_DATA = ( + ('aborted', AbortedResult(state=State(term=int_dv(1)), depth=3, unknown_predicate=None, logs=()), True, 3), + ('normal', StuckResult(state=State(term=int_dv(2)), depth=1, logs=()), False, 1), +) -def test_execute_not_aborted_on_normal_result() -> None: - # Given - cts = _cterm_symbolic(StuckResult(state=State(term=int_dv(2)), depth=1, logs=())) - dummy: CTerm = Mock() +@pytest.mark.parametrize( + 'test_id,response,expected_aborted,expected_depth', _ABORT_SURFACE_DATA, ids=[d[0] for d in _ABORT_SURFACE_DATA] +) +def test_execute_surfaces_abort_when_not_raising( + test_id: str, response: object, expected_aborted: bool, expected_depth: int +) -> None: + # With raise_on_aborted=False, the CTermExecute.aborted flag reflects whether the backend aborted. + cts = _cterm_symbolic(response) - # When - result = cts.execute(dummy, raise_on_aborted=False) + result = cts.execute(Mock(), raise_on_aborted=False) - # Then - assert not result.aborted - assert result.depth == 1 + assert result.aborted is expected_aborted + assert result.depth == expected_depth + assert not result.vacuous @pytest.mark.parametrize('indeterminate', [True, False, None], ids=['true', 'false', 'absent']) diff --git a/pyk/src/tests/unit/kcfg/test_explore.py b/pyk/src/tests/unit/kcfg/test_explore.py index 61af75ee56..61626d8764 100644 --- a/pyk/src/tests/unit/kcfg/test_explore.py +++ b/pyk/src/tests/unit/kcfg/test_explore.py @@ -1,15 +1,19 @@ from __future__ import annotations +from typing import TYPE_CHECKING from unittest.mock import Mock import pytest from pyk.cterm.symbolic import CTermExecute from pyk.kcfg.explore import KCFGExplore -from pyk.kcfg.kcfg import NoProgress, Producer, Step +from pyk.kcfg.kcfg import NoProgress, Step from ..test_kcfg import term +if TYPE_CHECKING: + from pyk.kcfg.kcfg import KCFGExtendResult + def _explore(exec_result: CTermExecute) -> KCFGExplore: cterm_symbolic = Mock() @@ -18,67 +22,23 @@ def _explore(exec_result: CTermExecute) -> KCFGExplore: return KCFGExplore(cterm_symbolic) -def test_extend_cterm_reports_no_progress_not_stuck() -> None: - # Given a backend that makes no progress (depth 0, no next states, not vacuous) - cterm = term(1) - explore = _explore(CTermExecute(state=cterm, next_states=(), depth=0, vacuous=False, aborted=False, logs=())) - - # When - results = explore.extend_cterm(cterm, node_id=1) - - # Then the worker emits the neutral NoProgress signal — never Stuck (the coordinator decides) - assert len(results) == 1 - assert isinstance(results[0], NoProgress) - - -def test_extend_cterm_step_on_progress() -> None: - # Given a backend that makes progress - cterm = term(1) - nxt = term(2) - explore = _explore(CTermExecute(state=nxt, next_states=(), depth=3, vacuous=False, aborted=False, logs=())) - - # When - results = explore.extend_cterm(cterm, node_id=1) - - # Then a basic-block Step is produced (unchanged behaviour) - assert len(results) == 1 - assert isinstance(results[0], Step) - - -@pytest.mark.parametrize( - 'booster_only,expected_producer', - [(True, Producer.BOOSTER_SIMPLIFY), (False, Producer.KORE_SIMPLIFY)], - ids=['booster', 'kore'], +# A zero-depth no-op execute yields the neutral NoProgress (never Stuck — the coordinator decides); +# a progressing execute yields a basic-block Step (unchanged behaviour). +_EXTEND_DATA: tuple[tuple[str, CTermExecute, type[KCFGExtendResult]], ...] = ( + ( + 'no-progress', + CTermExecute(state=term(1), next_states=(), depth=0, vacuous=False, aborted=False, logs=()), + NoProgress, + ), + ('progress', CTermExecute(state=term(2), next_states=(), depth=3, vacuous=False, aborted=False, logs=()), Step), ) -def test_simplify_variant_producer_and_capture(booster_only: bool, expected_producer: Producer) -> None: - # Given a cterm_symbolic that simplifies to a new term and exposes the request id - cterm_symbolic = Mock() - cterm_symbolic.simplify.return_value = (term(2), ()) - cterm_symbolic.last_request_id = 'claim-001' - explore = KCFGExplore(cterm_symbolic) - - # When - variant = explore.simplify_variant(term(1), booster_only=booster_only) - - # Then the producer matches the backend, and the request_id is captured - assert variant.producer is expected_producer - assert variant.cterm == term(2) - assert variant.request_id == 'claim-001' - # And the simplify was invoked with the right backend - _args, kwargs = cterm_symbolic.simplify.call_args - assert kwargs['booster_only_simplify'] is booster_only -def test_simplify_variant_noop_still_yields_variant() -> None: - # Given a no-op simplification (term unchanged) - cterm_symbolic = Mock() - cterm_symbolic.simplify.return_value = (term(1), ()) - cterm_symbolic.last_request_id = 'claim-002' - explore = KCFGExplore(cterm_symbolic) - - # When - variant = explore.simplify_variant(term(1), booster_only=True) - - # Then a variant is still produced, whose cterm equals the input (the no-op is recorded) - assert variant.cterm == term(1) - assert variant.producer is Producer.BOOSTER_SIMPLIFY +@pytest.mark.parametrize('test_id,exec_result,expected', _EXTEND_DATA, ids=[d[0] for d in _EXTEND_DATA]) +def test_extend_cterm_classifies_execute_result( + test_id: str, exec_result: CTermExecute, expected: type[KCFGExtendResult] +) -> None: + explore = _explore(exec_result) + results = explore.extend_cterm(term(1), node_id=1) + assert len(results) == 1 + assert isinstance(results[0], expected) diff --git a/pyk/src/tests/unit/test_kcfg.py b/pyk/src/tests/unit/test_kcfg.py index 0cecea82e0..593e1e57e2 100644 --- a/pyk/src/tests/unit/test_kcfg.py +++ b/pyk/src/tests/unit/test_kcfg.py @@ -14,7 +14,7 @@ from pyk.kast.prelude.utils import token from pyk.kast.pretty import PrettyPrinter from pyk.kcfg import KCFG, KCFGShow -from pyk.kcfg.kcfg import KCFGNodeAttr +from pyk.kcfg.kcfg import KCFGNodeAttr, NodeVariant, Producer from pyk.kcfg.show import NodePrinter from pyk.utils import not_none, single @@ -252,20 +252,42 @@ def test_create_node() -> None: assert not cfg.is_stuck(new_node.id) -def test_node_variants_default_empty_and_roundtrip() -> None: - # Given a node built the legacy way - n = node(1) +_NODE_ROUNDTRIP_DATA: tuple[tuple[str, KCFG.Node], ...] = ( + ('bare', KCFG.Node(1, term(1))), + ( + 'with-variants', + KCFG.Node( + 1, + term(2), + variants=[ + NodeVariant(Producer.INIT, None, term(1)), + NodeVariant(Producer.BOOSTER_SIMPLIFY, 'r-1', term(2)), + ], + ), + ), + ('with-attrs', KCFG.Node(1, term(1), attrs=[KCFGNodeAttr.BOOSTER_TRIED, KCFGNodeAttr.SUBSUME_INDETERMINATE])), +) - # Then variants default to empty and the serialised form omits the key - assert n.variants == () - assert 'variants' not in n.to_dict() - # And a legacy node dict (no 'variants') still loads - assert KCFG.Node.from_dict(n.to_dict()) == n +@pytest.mark.parametrize('test_id,node', _NODE_ROUNDTRIP_DATA, ids=[d[0] for d in _NODE_ROUNDTRIP_DATA]) +def test_node_serialisation_roundtrip(test_id: str, node: KCFG.Node) -> None: + # Node.to_dict/from_dict round-trips attrs and the variant chain; node equality ignores variants, + # so the chain is compared explicitly. + restored = KCFG.Node.from_dict(node.to_dict()) + assert restored == node + assert restored.variants == node.variants -def test_add_variant_chains_and_updates_cterm() -> None: - from pyk.kcfg.kcfg import Producer +def test_serialisation_omits_empty_recover_keys() -> None: + # Additive/back-compat: recover-mode keys are absent when empty, so legacy readers are unaffected. + assert 'variants' not in KCFG.Node(1, term(1)).to_dict() + cfg = KCFG() + cfg.create_node(term(1)) + assert 'kore_handoffs' not in cfg.to_dict() + assert 'kore_handoffs' not in cfg.to_dict_no_nodes() + + +def test_add_variant_chains_and_updates_cterm() -> None: # Given a fresh node at rung 0 cfg = KCFG() n = cfg.create_node(term(1)) @@ -292,26 +314,7 @@ def test_add_variant_chains_and_updates_cterm() -> None: ] -def test_node_variants_to_dict_from_dict_roundtrip() -> None: - from pyk.kcfg.kcfg import Producer - - # Given a node carrying a variant chain - cfg = KCFG() - n = cfg.create_node(term(1)) - cfg.add_variant(n.id, Producer.BOOSTER_SIMPLIFY, term(2), request_id='r-1') - original = cfg.node(n.id) - - # When round-tripped through dict - restored = KCFG.Node.from_dict(original.to_dict()) - - # Then variants survive (equality ignores variants, so compare them explicitly) - assert restored == original - assert restored.variants == original.variants - - def test_node_equality_ignores_variants() -> None: - from pyk.kcfg.kcfg import NodeVariant, Producer - # Given two nodes identical but for their variant chains bare = KCFG.Node(1, term(1)) with_variants = KCFG.Node(1, term(1), variants=[NodeVariant(Producer.INIT, None, term(1))]) @@ -336,29 +339,6 @@ def test_kore_handoffs_add_and_roundtrip() -> None: assert restored.kore_handoffs == cfg.kore_handoffs -def test_kore_handoffs_omitted_when_empty() -> None: - # Given a kcfg with no handoffs - cfg = KCFG() - cfg.create_node(term(1)) - - # Then the key is omitted from both serialisations (additive / back-compat) - assert 'kore_handoffs' not in cfg.to_dict() - assert 'kore_handoffs' not in cfg.to_dict_no_nodes() - - -def test_recover_mode_node_attrs_serialise() -> None: - # Given a node carrying the new recover-mode attrs - cfg = KCFG() - n = cfg.create_node(term(1)) - cfg.add_attr(n.id, KCFGNodeAttr.BOOSTER_TRIED) - cfg.add_attr(n.id, KCFGNodeAttr.SUBSUME_INDETERMINATE) - - # Then the attrs round-trip through the in-memory Node serialisation - restored = KCFG.Node.from_dict(cfg.node(n.id).to_dict()) - assert KCFGNodeAttr.BOOSTER_TRIED in restored.attrs - assert KCFGNodeAttr.SUBSUME_INDETERMINATE in restored.attrs - - def test_remove_unknown_node() -> None: # Given cfg = KCFG() diff --git a/pyk/src/tests/unit/test_proof.py b/pyk/src/tests/unit/test_proof.py index 556b01a49e..cd8873bc55 100644 --- a/pyk/src/tests/unit/test_proof.py +++ b/pyk/src/tests/unit/test_proof.py @@ -10,23 +10,18 @@ from pyk.kast.prelude.kbool import BOOL from pyk.kast.prelude.kint import intToken from pyk.kcfg.exploration import KCFGExplorationNodeAttr -from pyk.kcfg.kcfg import KCFG, HandoffFlavour, KCFGNodeAttr, KoreHandoff, NodeVariant, Producer, Step +from pyk.kcfg.kcfg import KCFG, KCFGNodeAttr, NodeVariant, Producer from pyk.proof import EqualityProof from pyk.proof.implies import EqualitySummary from pyk.proof.proof import CompositeSummary, Proof, ProofStatus from pyk.proof.reachability import ( APRFailureInfo, APRProof, - APRProofAddVariantResult, - APRProofRecoverAdvanceResult, - APRProofRecoverCloseResult, - APRProofRecoverNoProgressResult, APRProofStuckResult, APRProver, APRSummary, DecisiveInvalid, Indeterminate, - RecoverBackend, RecoverTask, Subsumed, recover_task_for, @@ -42,7 +37,6 @@ from pytest import TempPathFactory - from pyk.cterm import CTerm from pyk.kcfg.kcfg import NodeAttr from pyk.proof.reachability import SubsumptionCheck @@ -337,11 +331,17 @@ def _node_at_rung(rung: int, attrs: list[NodeAttr]) -> KCFG.Node: return KCFG.Node(1, term(rung + 1), attrs, chain) -def test_recovery_rung() -> None: - assert recovery_rung(KCFG.Node(1, term(1))) == 0 - assert recovery_rung(_node_at_rung(0, [])) == 0 - assert recovery_rung(_node_at_rung(1, [])) == 1 - assert recovery_rung(_node_at_rung(2, [])) == 2 +_RUNG_DATA: tuple[tuple[str, KCFG.Node, int], ...] = ( + ('bare-node', KCFG.Node(1, term(1)), 0), + ('empty-chain', _node_at_rung(0, []), 0), + ('booster-simplified', _node_at_rung(1, []), 1), + ('kore-simplified', _node_at_rung(2, []), 2), +) + + +@pytest.mark.parametrize('test_id,node,expected', _RUNG_DATA, ids=[d[0] for d in _RUNG_DATA]) +def test_recovery_rung(test_id: str, node: KCFG.Node, expected: int) -> None: + assert recovery_rung(node) == expected _TASK_DATA: tuple[tuple[str, int, list[NodeAttr], RecoverTask], ...] = ( @@ -360,140 +360,6 @@ def test_recover_task_selection(test_id: str, rung: int, attrs: list[NodeAttr], assert recover_task_for(_node_at_rung(rung, attrs)) is expected -def test_recover_task_noop_shortcircuit() -> None: - # After a no-op SIMPLIFY_BOOSTER, the term advanced to rung 1 but BOOSTER_TRIED stays set - # (commit's clear-iff-changed invariant), so the next task skips the redundant TRY_BOOSTER and - # goes straight to SIMPLIFY_KORE. - node = _node_at_rung(1, [KCFGNodeAttr.BOOSTER_TRIED]) - assert recover_task_for(node) is RecoverTask.SIMPLIFY_KORE - - -# --- commit recover transitions ------------------------------------------------------------------ - - -def _recover_proof() -> tuple[APRProof, int]: - kcfg = KCFG() - n_init = kcfg.create_node(term(1)) - n_target = kcfg.create_node(term(2)) - n = kcfg.create_node(term(3)) - proof = APRProof(id='rec', kcfg=kcfg, terminal=[], init=n_init.id, target=n_target.id, logs={}) - return proof, n.id - - -def _no_progress(node_id: int, backend: str, indeterminate: bool = False) -> APRProofRecoverNoProgressResult: - return APRProofRecoverNoProgressResult( - node_id=node_id, - prior_loops_cache_update=(), - optimize_kcfg=False, - backend=RecoverBackend(backend), - subsume_indeterminate=indeterminate, - ) - - -def _add_variant(node_id: int, producer: Producer, cterm: CTerm) -> APRProofAddVariantResult: - return APRProofAddVariantResult( - node_id=node_id, - prior_loops_cache_update=(), - optimize_kcfg=False, - producer=producer, - cterm=cterm, - request_id='r', - ) - - -def test_commit_no_progress_sets_booster_tried_and_indeterminate() -> None: - proof, nid = _recover_proof() - proof.commit(_no_progress(nid, 'booster', indeterminate=True)) - attrs = proof.kcfg.node(nid).attrs - assert KCFGNodeAttr.BOOSTER_TRIED in attrs - assert KCFGNodeAttr.SUBSUME_INDETERMINATE in attrs - assert not proof.kcfg.is_stuck(nid) - - -def test_commit_add_variant_clear_iff_changed() -> None: - proof, nid = _recover_proof() - proof.commit(_no_progress(nid, 'booster', indeterminate=True)) - - # No-op simplify (term unchanged): BOOSTER_TRIED stays set → short-circuit to next rung - proof.commit(_add_variant(nid, Producer.BOOSTER_SIMPLIFY, term(3))) - assert KCFGNodeAttr.BOOSTER_TRIED in proof.kcfg.node(nid).attrs - assert recovery_rung(proof.kcfg.node(nid)) == 1 - - # A term-changing simplify clears the per-rung try attrs - proof.commit(_add_variant(nid, Producer.KORE_SIMPLIFY, term(99))) - cleared = proof.kcfg.node(nid).attrs - assert KCFGNodeAttr.BOOSTER_TRIED not in cleared - assert KCFGNodeAttr.SUBSUME_INDETERMINATE not in cleared - assert recovery_rung(proof.kcfg.node(nid)) == 2 - - -def test_commit_full_ladder_to_both_backends_failed() -> None: - proof, nid = _recover_proof() - # rung 0: booster try fails (indeterminate), booster simplify changes the term → rung 1 - proof.commit(_no_progress(nid, 'booster', indeterminate=True)) - proof.commit(_add_variant(nid, Producer.BOOSTER_SIMPLIFY, term(10))) - # rung 1: booster try fails, kore simplify changes the term → rung 2 - proof.commit(_no_progress(nid, 'booster')) - proof.commit(_add_variant(nid, Producer.KORE_SIMPLIFY, term(20))) - # rung 2: booster try fails, then kore try fails → both backends exhausted - proof.commit(_no_progress(nid, 'booster')) - assert not proof.kcfg.is_stuck(nid) - proof.commit(_no_progress(nid, 'kore')) - - node = proof.kcfg.node(nid) - assert KCFGNodeAttr.BOTH_BACKENDS_FAILED in node.attrs - assert proof.kcfg.is_stuck(nid) - - -def test_commit_recover_close_records_implies_handoff() -> None: - proof, nid = _recover_proof() - proof.commit( - APRProofRecoverCloseResult( - node_id=nid, - prior_loops_cache_update=(), - optimize_kcfg=False, - csubst=CSubst(), - kore_request_id='r-imp', - ) - ) - assert proof.kcfg.kore_handoffs == [ - KoreHandoff(source=nid, target=proof.target, flavour=HandoffFlavour.IMPLIES, request_id='r-imp') - ] - - -def test_commit_recover_advance_records_execute_handoff() -> None: - proof, nid = _recover_proof() - proof.commit( - APRProofRecoverAdvanceResult( - node_id=nid, - prior_loops_cache_update=(), - optimize_kcfg=False, - extension_to_apply=Step(term(50), 1, (), []), - kore_request_id='r-exec', - ) - ) - handoffs = proof.kcfg.kore_handoffs - assert len(handoffs) == 1 - assert handoffs[0].flavour == HandoffFlavour.EXECUTE - assert handoffs[0].source == nid - assert handoffs[0].request_id == 'r-exec' - - -def test_commit_recover_advance_no_handoff_for_booster() -> None: - # A booster advance (kore_request_id None) records no handoff. - proof, nid = _recover_proof() - proof.commit( - APRProofRecoverAdvanceResult( - node_id=nid, - prior_loops_cache_update=(), - optimize_kcfg=False, - extension_to_apply=Step(term(50), 1, (), []), - kore_request_id=None, - ) - ) - assert proof.kcfg.kore_handoffs == [] - - def test_apr_proof_minimization_and_terminals() -> None: # 25 /-- X >=Int 5 --> 10 # 5 10 15 20 /-- X >=Int 0 --> 6 --> 8 From 29fd186a3a527f9943f2fabfafce3b78b302b294 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 10 Jun 2026 04:12:16 +0000 Subject: [PATCH 22/26] proof/reachability, tests/unit/test_proof: short-circuit #Bottom cterms 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 --- pyk/src/pyk/proof/reachability.py | 18 +++++++++++++++++- pyk/src/tests/unit/test_proof.py | 24 ++++++++++++++++++++++-- 2 files changed, 39 insertions(+), 3 deletions(-) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index ce0572be67..a6b2ac084a 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -15,7 +15,7 @@ from ..kast.prelude.ml import mlAnd, mlTop from ..kcfg import KCFG, KCFGStore from ..kcfg.exploration import KCFGExploration -from ..kcfg.kcfg import HandoffFlavour, KCFGNodeAttr, KoreHandoff, NoProgress, Producer +from ..kcfg.kcfg import HandoffFlavour, KCFGNodeAttr, KoreHandoff, NoProgress, Producer, Vacuous from ..kore.rpc import LogEntry, client_label from ..ktool.claim_index import ClaimIndex from ..utils import FrozenDict, ensure_dir_path, hash_str, shorten_hashes, single @@ -1046,6 +1046,22 @@ def _check_subsume( return Indeterminate() if result.indeterminate else DecisiveInvalid() def step_proof(self, step: APRProofStep) -> list[APRProofResult]: + # Recover-mode only: a booster-only re-simplify can collapse a node's configuration to bare + # `#Bottom`, which has no destructurable cells, so any semantics callback (`is_loop`, + # `is_terminal`, ...) may crash on it. Short-circuit to the same `Vacuous` judgment + # `commit` applies on the normal path — there `extend_cterm` owns vacuity detection and a + # bottom configuration never lands in a node, but the recover ladder's `add_variant` + # bypasses that path. + if step.recover_task is not None and step.node.cterm.is_bottom: + return [ + APRProofExtendResult( + node_id=step.node.id, + extension_to_apply=Vacuous(), + prior_loops_cache_update=(), + optimize_kcfg=self.optimize_kcfg, + ) + ] + # Check if the current node should be bounded prior_loops: tuple[int, ...] = () if step.bmc_depth is not None and self.kcfg_explore.kcfg_semantics.is_loop(step.node.cterm): diff --git a/pyk/src/tests/unit/test_proof.py b/pyk/src/tests/unit/test_proof.py index cd8873bc55..c3fdcdf88b 100644 --- a/pyk/src/tests/unit/test_proof.py +++ b/pyk/src/tests/unit/test_proof.py @@ -5,18 +5,19 @@ import pytest -from pyk.cterm import CSubst +from pyk.cterm import CSubst, CTerm from pyk.cterm.symbolic import CTermImplies from pyk.kast.prelude.kbool import BOOL from pyk.kast.prelude.kint import intToken from pyk.kcfg.exploration import KCFGExplorationNodeAttr -from pyk.kcfg.kcfg import KCFG, KCFGNodeAttr, NodeVariant, Producer +from pyk.kcfg.kcfg import KCFG, KCFGNodeAttr, NodeVariant, Producer, Vacuous from pyk.proof import EqualityProof from pyk.proof.implies import EqualitySummary from pyk.proof.proof import CompositeSummary, Proof, ProofStatus from pyk.proof.reachability import ( APRFailureInfo, APRProof, + APRProofExtendResult, APRProofStuckResult, APRProver, APRSummary, @@ -360,6 +361,25 @@ def test_recover_task_selection(test_id: str, rung: int, attrs: list[NodeAttr], assert recover_task_for(_node_at_rung(rung, attrs)) is expected +def test_recover_step_bottom_node_judged_vacuous() -> None: + # Given a recover-mode step whose node configuration collapsed to bare #Bottom + # (a booster-only re-simplify of a vacuous node can land one via add_variant) + prover = Mock() + prover.optimize_kcfg = False + step = Mock(node=Mock(id=1, cterm=CTerm.bottom()), recover_task=RecoverTask.TRY_BOOSTER) + + # When (call the unbound method with the Mock as self) + results = APRProver.step_proof(prover, step) + + # Then the node is judged vacuous without consulting the semantics, whose callbacks + # may destructure cells that a bottom configuration does not have + assert results == [ + APRProofExtendResult(node_id=1, extension_to_apply=Vacuous(), prior_loops_cache_update=(), optimize_kcfg=False) + ] + prover.kcfg_explore.kcfg_semantics.is_loop.assert_not_called() + prover.kcfg_explore.kcfg_semantics.is_terminal.assert_not_called() + + def test_apr_proof_minimization_and_terminals() -> None: # 25 /-- X >=Int 5 --> 10 # 5 10 15 20 /-- X >=Int 0 --> 6 --> 8 From 7c10252ebbb3ce3d5735602f65e6580c936e589e Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 10 Jun 2026 18:47:35 +0000 Subject: [PATCH 23/26] cterm/symbolic: drop unused CTermExecute.aborted flag 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 --- pyk/src/pyk/cterm/symbolic.py | 12 ++++-------- pyk/src/tests/unit/cterm/test_symbolic.py | 14 ++++++-------- pyk/src/tests/unit/kcfg/test_explore.py | 4 ++-- 3 files changed, 12 insertions(+), 18 deletions(-) diff --git a/pyk/src/pyk/cterm/symbolic.py b/pyk/src/pyk/cterm/symbolic.py index 3bbe7ce1eb..cb5436802a 100644 --- a/pyk/src/pyk/cterm/symbolic.py +++ b/pyk/src/pyk/cterm/symbolic.py @@ -71,7 +71,6 @@ class CTermExecute(NamedTuple): next_states: tuple[NextState, ...] depth: int vacuous: bool - aborted: bool logs: tuple[LogEntry, ...] @@ -200,12 +199,10 @@ def execute( # Under booster-only execution, an `AbortedResult` is the expected signal that the booster # could make no further progress (it is what drives the recover-mode ladder). Callers that - # want to inspect the abort rather than treat it as fatal pass `raise_on_aborted=False`; the - # `AbortedResult.reason`/`next_states` class attributes let the rest of this body proceed - # unchanged, surfacing `aborted=True` on the result. - aborted = isinstance(response, AbortedResult) - if aborted and raise_on_aborted: - assert isinstance(response, AbortedResult) + # expect aborts pass `raise_on_aborted=False`; the `AbortedResult.reason`/`next_states` + # class attributes let the rest of this body proceed unchanged, and a no-progress abort + # surfaces as a depth-0 result. + if raise_on_aborted and isinstance(response, AbortedResult): unknown_predicate = response.unknown_predicate.text if response.unknown_predicate else None raise ValueError(f'Backend responded with aborted state. Unknown predicate: {unknown_predicate}') @@ -228,7 +225,6 @@ def execute( next_states=next_states, depth=response.depth, vacuous=response.reason is StopReason.VACUOUS, - aborted=aborted, logs=response.logs, ) diff --git a/pyk/src/tests/unit/cterm/test_symbolic.py b/pyk/src/tests/unit/cterm/test_symbolic.py index 61d284e6a4..2ff5fc0ca2 100644 --- a/pyk/src/tests/unit/cterm/test_symbolic.py +++ b/pyk/src/tests/unit/cterm/test_symbolic.py @@ -39,23 +39,21 @@ def test_execute_raises_on_abort_by_default() -> None: _ABORT_SURFACE_DATA = ( - ('aborted', AbortedResult(state=State(term=int_dv(1)), depth=3, unknown_predicate=None, logs=()), True, 3), - ('normal', StuckResult(state=State(term=int_dv(2)), depth=1, logs=()), False, 1), + ('aborted', AbortedResult(state=State(term=int_dv(1)), depth=3, unknown_predicate=None, logs=()), 3), + ('normal', StuckResult(state=State(term=int_dv(2)), depth=1, logs=()), 1), ) @pytest.mark.parametrize( - 'test_id,response,expected_aborted,expected_depth', _ABORT_SURFACE_DATA, ids=[d[0] for d in _ABORT_SURFACE_DATA] + 'test_id,response,expected_depth', _ABORT_SURFACE_DATA, ids=[d[0] for d in _ABORT_SURFACE_DATA] ) -def test_execute_surfaces_abort_when_not_raising( - test_id: str, response: object, expected_aborted: bool, expected_depth: int -) -> None: - # With raise_on_aborted=False, the CTermExecute.aborted flag reflects whether the backend aborted. +def test_execute_tolerates_abort_when_not_raising(test_id: str, response: object, expected_depth: int) -> None: + # With raise_on_aborted=False, an aborted response is not fatal and surfaces as an ordinary + # result (a no-progress abort comes back as depth 0). cts = _cterm_symbolic(response) result = cts.execute(Mock(), raise_on_aborted=False) - assert result.aborted is expected_aborted assert result.depth == expected_depth assert not result.vacuous diff --git a/pyk/src/tests/unit/kcfg/test_explore.py b/pyk/src/tests/unit/kcfg/test_explore.py index 61626d8764..dbab4b429c 100644 --- a/pyk/src/tests/unit/kcfg/test_explore.py +++ b/pyk/src/tests/unit/kcfg/test_explore.py @@ -27,10 +27,10 @@ def _explore(exec_result: CTermExecute) -> KCFGExplore: _EXTEND_DATA: tuple[tuple[str, CTermExecute, type[KCFGExtendResult]], ...] = ( ( 'no-progress', - CTermExecute(state=term(1), next_states=(), depth=0, vacuous=False, aborted=False, logs=()), + CTermExecute(state=term(1), next_states=(), depth=0, vacuous=False, logs=()), NoProgress, ), - ('progress', CTermExecute(state=term(2), next_states=(), depth=3, vacuous=False, aborted=False, logs=()), Step), + ('progress', CTermExecute(state=term(2), next_states=(), depth=3, vacuous=False, logs=()), Step), ) From 92b77d3387a57640831b33a8301f8768d9a9583c Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 10 Jun 2026 18:47:55 +0000 Subject: [PATCH 24/26] kore/rpc: drop drive-by MultipleStatesError (code 7) mapping 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 --- pyk/src/pyk/kore/rpc.py | 17 ----------------- pyk/src/tests/unit/kore/test_client.py | 7 ------- 2 files changed, 24 deletions(-) diff --git a/pyk/src/pyk/kore/rpc.py b/pyk/src/pyk/kore/rpc.py index 294e6723f2..f220b1ee5d 100644 --- a/pyk/src/pyk/kore/rpc.py +++ b/pyk/src/pyk/kore/rpc.py @@ -467,21 +467,6 @@ def __init__(self, data: str): super().__init__(f'Backend aborted: {self.data}') -@final -@dataclass -class MultipleStatesError(KoreClientError): - """The backend returned multiple states where one was expected (JSON-RPC ``code: 7``). - - ``data`` is the accompanying reason text. - """ - - data: str - - def __init__(self, data: str): - self.data = data - super().__init__(f'Multiple states: {self.data}') - - @final @dataclass class DefaultError(KoreClientError): @@ -1073,8 +1058,6 @@ def _error(self, err: JsonRpcError) -> KoreClientError: return SmtSolverError(error=err.data['error'], pattern=kore_term(err.data['term'])) case 6: return AbortedError(data=err.data) - case 7: - return MultipleStatesError(data=err.data) case 8: return InvalidModuleError(error=err.data['error'], context=err.data.get('context')) case 9: diff --git a/pyk/src/tests/unit/kore/test_client.py b/pyk/src/tests/unit/kore/test_client.py index 37f24e3a24..f602c1821e 100644 --- a/pyk/src/tests/unit/kore/test_client.py +++ b/pyk/src/tests/unit/kore/test_client.py @@ -17,7 +17,6 @@ JsonRpcError, KoreClient, KoreClientError, - MultipleStatesError, ParseError, PatternError, SatResult, @@ -408,12 +407,6 @@ def test_add_module( AbortedError(data='unknown constraints'), 'Backend aborted: unknown constraints', ), - ( - 'multiple-states-error', - JsonRpcError(message='Multiple states', code=7, data='more than one state'), - MultipleStatesError(data='more than one state'), - 'Multiple states: more than one state', - ), ( 'default-error', JsonRpcError(message='foo', code=100, data={'bar': 1, 'baz': [2, 3]}), From b441bc27306d22c146560e954201228816489d24 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 10 Jun 2026 18:48:15 +0000 Subject: [PATCH 25/26] kcfg/store: drop stale design-doc reference from OptimizedNodeStore comment Co-Authored-By: Claude Fable 5 --- pyk/src/pyk/kcfg/store.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyk/src/pyk/kcfg/store.py b/pyk/src/pyk/kcfg/store.py index 5661e3ffbd..40644a4738 100644 --- a/pyk/src/pyk/kcfg/store.py +++ b/pyk/src/pyk/kcfg/store.py @@ -40,7 +40,7 @@ def __getitem__(self, key: int) -> KCFG.Node: def __setitem__(self, key: int, node: KCFG.Node) -> None: # Term-dedup the canonical cterm and every variant cterm, carrying the provenance chain - # through unchanged (variants must survive the store, see C8). + # through unchanged (variants must survive the store). new_variants = tuple( NodeVariant(variant.producer, variant.request_id, self._optimize_cterm(variant.cterm)) for variant in node.variants From e07822f531e95020c7b13768af0d87b30ca08b63 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 10 Jun 2026 20:43:22 +0000 Subject: [PATCH 26/26] kore/rpc, cterm/symbolic, proof/reachability: drop speculative ImpliesResult.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 --- pyk/src/pyk/cterm/symbolic.py | 13 ++++++----- pyk/src/pyk/kore/rpc.py | 5 ---- pyk/src/pyk/proof/reachability.py | 4 ++-- pyk/src/tests/unit/cterm/test_symbolic.py | 28 +---------------------- pyk/src/tests/unit/kore/test_client.py | 19 --------------- pyk/src/tests/unit/test_proof.py | 5 ++-- 6 files changed, 12 insertions(+), 62 deletions(-) diff --git a/pyk/src/pyk/cterm/symbolic.py b/pyk/src/pyk/cterm/symbolic.py index cb5436802a..7a97f32e51 100644 --- a/pyk/src/pyk/cterm/symbolic.py +++ b/pyk/src/pyk/cterm/symbolic.py @@ -79,7 +79,9 @@ class CTermImplies(NamedTuple): failing_cells: tuple[tuple[str, KInner], ...] remaining_implication: KInner | None logs: tuple[LogEntry, ...] - indeterminate: bool | None = None + # True when the backend aborted the implies (it could not decide it) — a couldn't-determine, + # not a decisive verdict. Recover-mode escalates on it instead of trusting `csubst is None`. + indeterminate: bool = False @final @@ -335,9 +337,8 @@ def implies( except SmtSolverError as err: raise self._smt_solver_error(err) from err except AbortedError as err: - # kore-implies aborted because it could not decide the implication (e.g. constraints - # the engine cannot discharge). Surface it as an indeterminate, not-subsumed result — - # uniform with how booster-implies reports a MatchIndeterminate (`indeterminate=True`) — + # The backend aborted because it could not decide the implication (e.g. constraints + # the engine cannot discharge). Surface it as an indeterminate, not-subsumed result, # so callers (notably recover-mode's TRY_KORE escalation, which calls kore-implies # directly and so sees the raw abort the proxy would otherwise absorb) treat it as # "unknown" instead of crashing. @@ -388,7 +389,7 @@ def implies( ) ) remaining_implication = CTerm._ml_impl(antecedent.constraints, consequent_constraints) - return CTermImplies(None, tuple(failing_cells), remaining_implication, result.logs, result.indeterminate) + return CTermImplies(None, tuple(failing_cells), remaining_implication, result.logs) if result.substitution is None: raise ValueError('Received empty substutition for valid implication.') @@ -398,7 +399,7 @@ def implies( ml_pred = self.kore_to_kast(result.predicate) ml_subst_pred = mlAnd(flatten_label('#And', ml_subst) + flatten_label('#And', ml_pred)) csubst = CSubst.from_pred(ml_subst_pred) - return CTermImplies(csubst, (), None, result.logs, result.indeterminate) + return CTermImplies(csubst, (), None, result.logs) def assume_defined( self, cterm: CTerm, module_name: str | None = None, booster_only_simplify: bool = False diff --git a/pyk/src/pyk/kore/rpc.py b/pyk/src/pyk/kore/rpc.py index f220b1ee5d..2a5871695a 100644 --- a/pyk/src/pyk/kore/rpc.py +++ b/pyk/src/pyk/kore/rpc.py @@ -913,10 +913,6 @@ class ImpliesResult: predicate: Pattern | None logs: tuple[LogEntry, ...] haskell_log_entries: tuple[Any, ...] | None = None - # `Just True` only on booster's MatchIndeterminate-no-progress paths; absent (⇒ None) on - # every decisive `valid` verdict and every error. Lets a caller tell a decisive invalid - # (trust) from a couldn't-determine (escalate to kore). See booster `f911be4e0`. - indeterminate: bool | None = None @staticmethod def from_dict(dct: Mapping[str, Any]) -> ImpliesResult: @@ -930,7 +926,6 @@ def from_dict(dct: Mapping[str, Any]) -> ImpliesResult: predicate=kore_term(predicate) if predicate is not None else None, logs=logs, haskell_log_entries=_parse_haskell_log_entries(dct), - indeterminate=dct.get('indeterminate'), ) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index a6b2ac084a..bc7b5d1bb5 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -1041,8 +1041,8 @@ def _check_subsume( if result.csubst is not None: _LOGGER.info(f'Subsumed into target node {proof_id}: {shorten_hashes((node.id, target_node.id))}') return Subsumed(result.csubst) - # Not subsumed: a decisive invalid is trusted; a couldn't-determine (booster - # `MatchIndeterminate`) is surfaced so recover-mode can escalate to a kore implies. + # Not subsumed: a decisive invalid is trusted; a couldn't-determine (an aborted implies) + # is surfaced so recover-mode can escalate to a kore implies. return Indeterminate() if result.indeterminate else DecisiveInvalid() def step_proof(self, step: APRProofStep) -> list[APRProofResult]: diff --git a/pyk/src/tests/unit/cterm/test_symbolic.py b/pyk/src/tests/unit/cterm/test_symbolic.py index 2ff5fc0ca2..6c104ad259 100644 --- a/pyk/src/tests/unit/cterm/test_symbolic.py +++ b/pyk/src/tests/unit/cterm/test_symbolic.py @@ -8,7 +8,7 @@ from pyk.cterm.symbolic import CTermSymbolic from pyk.kast.prelude.ml import mlTop from pyk.kore.prelude import int_dv -from pyk.kore.rpc import AbortedError, AbortedResult, ImpliesResult, State, StuckResult +from pyk.kore.rpc import AbortedError, AbortedResult, State, StuckResult if TYPE_CHECKING: from pyk.cterm import CTerm @@ -58,32 +58,6 @@ def test_execute_tolerates_abort_when_not_raising(test_id: str, response: object assert not result.vacuous -@pytest.mark.parametrize('indeterminate', [True, False, None], ids=['true', 'false', 'absent']) -def test_implies_surfaces_indeterminate(indeterminate: bool | None) -> None: - # Given a falsifiable implication carrying the backend `indeterminate` flag - kore_client = Mock() - kore_client.implies.return_value = ImpliesResult( - valid=False, - implication=Mock(), - substitution=None, - predicate=None, - logs=(), - indeterminate=indeterminate, - ) - cts = CTermSymbolic(kore_client, Mock()) - cts.kast_to_kore = Mock(return_value=Mock()) # type: ignore[method-assign] - # Stub CTerm operands: no free vars (so no consequent binding), arbitrary kast. - antecedent: CTerm = Mock(free_vars=frozenset()) - consequent: CTerm = Mock(free_vars=frozenset()) - - # When - result = cts.implies(antecedent, consequent) - - # Then - assert result.csubst is None - assert result.indeterminate is indeterminate - - def test_implies_aborted_treated_as_indeterminate() -> None: # Given a backend whose implies aborts (kore-rpc `code: 6`, e.g. recover-mode's direct # kore-implies call hitting "unknown constraints" the proxy would otherwise absorb) diff --git a/pyk/src/tests/unit/kore/test_client.py b/pyk/src/tests/unit/kore/test_client.py index f602c1821e..60aa9b89cb 100644 --- a/pyk/src/tests/unit/kore/test_client.py +++ b/pyk/src/tests/unit/kore/test_client.py @@ -206,25 +206,6 @@ def test_implies( assert actual == expected -@pytest.mark.parametrize('indeterminate', [True, False, None], ids=['true', 'false', 'absent']) -def test_implies_parses_indeterminate( - kore_client: KoreClient, - rpc_client: MockClient, - indeterminate: bool | None, -) -> None: - # Given a falsifiable implication whose `indeterminate` flag varies (absent ⇒ omitted) - response: dict[str, Any] = {'valid': False, 'implication': kore(int_top)} - if indeterminate is not None: - response['indeterminate'] = indeterminate - rpc_client.assume_response(response) - - # When - actual = kore_client.implies(int_bottom, int_top) - - # Then - assert actual.indeterminate is indeterminate - - SIMPLIFY_TEST_DATA: Final = ( ( And(INT, (int_top, int_top)), diff --git a/pyk/src/tests/unit/test_proof.py b/pyk/src/tests/unit/test_proof.py index c3fdcdf88b..5bef7e6c2a 100644 --- a/pyk/src/tests/unit/test_proof.py +++ b/pyk/src/tests/unit/test_proof.py @@ -276,9 +276,8 @@ def test_commit_stuck_result_marks_node_stuck() -> None: _CSUBST_SENTINEL: Final = CSubst() _CHECK_SUBSUME_DATA: Final = ( - ('subsumed', _CSUBST_SENTINEL, None, Subsumed), + ('subsumed', _CSUBST_SENTINEL, False, Subsumed), ('decisive-invalid', None, False, DecisiveInvalid), - ('decisive-invalid-absent', None, None, DecisiveInvalid), ('indeterminate', None, True, Indeterminate), ) @@ -291,7 +290,7 @@ def test_commit_stuck_result_marks_node_stuck() -> None: def test_check_subsume_classification( test_id: str, csubst: CSubst | None, - indeterminate: bool | None, + indeterminate: bool, expected: type[SubsumptionCheck], ) -> None: # Given a prover whose implies returns a CTermImplies with the given csubst / indeterminate