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/cterm/symbolic.py b/pyk/src/pyk/cterm/symbolic.py index af8f9a4e36..7a97f32e51 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, @@ -78,6 +79,9 @@ class CTermImplies(NamedTuple): failing_cells: tuple[tuple[str, KInner], ...] remaining_implication: KInner | None logs: tuple[LogEntry, ...] + # 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 @@ -153,6 +157,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 by the backing client (see `KoreClient.last_request_id`). + + 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, cterm: CTerm, @@ -162,6 +176,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 +199,12 @@ 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 + # 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}') @@ -316,6 +336,14 @@ def implies( ) except SmtSolverError as err: raise self._smt_solver_error(err) from err + except AbortedError as err: + # 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. + _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/kcfg/explore.py b/pyk/src/pyk/kcfg/explore.py index 1eef51588a..549f833e43 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,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, Producer, Step, Vacuous from .semantics import DefaultSemantics if TYPE_CHECKING: @@ -35,6 +35,20 @@ _LOGGER: Final = logging.getLogger(__name__) +class SimplifyVariant(NamedTuple): + """Result of a recover-mode variant-producing simplification. + + 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 + + class KCFGExplore: cterm_symbolic: CTermSymbolic @@ -136,6 +150,22 @@ 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 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). 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) + return SimplifyVariant( + producer=producer, + cterm=simplified, + request_id=self.cterm_symbolic.last_request_id, + ) + def step( self, cfg: KCFG, @@ -218,6 +248,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]: @@ -229,14 +261,21 @@ 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, 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 + next_states = exec_result.next_states + depth = exec_result.depth + vacuous = exec_result.vacuous + next_node_logs = exec_result.logs extend_results: list[KCFGExtendResult] = [] @@ -244,12 +283,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. 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..9d02a2ce8a 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 @@ -49,11 +50,97 @@ 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): + """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 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 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: HandoffFlavour + request_id: str + + def to_dict(self) -> dict[str, Any]: + 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'], HandoffFlavour(dct['flavour']), dct['request_id']) 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. + _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) @@ -73,12 +160,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: @@ -88,21 +171,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 @@ -117,34 +201,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`. + 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]: @@ -439,6 +550,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: @@ -458,6 +571,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) @@ -638,6 +752,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} @@ -660,6 +775,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} @@ -697,6 +813,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]: @@ -856,6 +975,36 @@ 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 + + @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) @@ -1320,6 +1469,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/kcfg/store.py b/pyk/src/pyk/kcfg/store.py index 0488bf3778..40644a4738 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). + 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/pyk/kore/rpc.py b/pyk/src/pyk/kore/rpc.py index e4e0355883..2a5871695a 100644 --- a/pyk/src/pyk/kore/rpc.py +++ b/pyk/src/pyk/kore/rpc.py @@ -449,6 +449,24 @@ 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 DefaultError(KoreClientError): @@ -1033,6 +1051,8 @@ 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 8: return InvalidModuleError(error=err.data['error'], context=err.data.get('context')) case 9: 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/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 0b4a66d2b3..bc7b5d1bb5 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -3,8 +3,10 @@ import json import logging import re +from abc import ABC from dataclasses import dataclass, field -from typing import TYPE_CHECKING +from enum import Enum +from typing import TYPE_CHECKING, final from ..cterm.cterm import remove_useless_constraints from ..kast.inner import KInner, Subst @@ -13,6 +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, 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 @@ -24,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 @@ -34,6 +38,52 @@ _LOGGER: Final = logging.getLogger(__name__) +class RecoverTask(Enum): + """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. + """ + + TRY_BOOSTER = 'try-booster' + SIMPLIFY_BOOSTER = 'simplify-booster' + SIMPLIFY_KORE = 'simplify-kore' + 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). + + 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. + + 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 @@ -75,6 +125,81 @@ 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. + """ + + +@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 + + +@dataclass +class APRProofRecoverNoProgressResult(APRProofResult): + """Recover-mode: a `try` made no progress; `commit` sets the per-backend attr (and may stuck).""" + + backend: RecoverBackend + subsume_indeterminate: bool + + +@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 + + +@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 + + +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``. + """ + + +@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 @@ -88,6 +213,7 @@ class APRProofStep: circularity: bool nonzero_depth: bool circularity_rule_id: str + recover_task: RecoverTask | None = None class APRProof(Proof[APRProofStep, APRProofResult], KCFGExploration): @@ -113,6 +239,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] @@ -156,6 +285,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) @@ -197,12 +327,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). + 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), @@ -210,6 +349,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 @@ -240,11 +380,86 @@ 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. + _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=HandoffFlavour.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=HandoffFlavour.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: 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: + 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, + # 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) @@ -725,6 +940,7 @@ class APRProver(Prover[APRProof, APRProofStep, APRProofResult]): kcfg_explore: KCFGExplore extra_module: KFlatModule | None optimize_kcfg: bool + recover_mode: bool def __init__( self, @@ -738,6 +954,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 @@ -751,6 +968,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() @@ -762,6 +980,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) @@ -798,19 +1020,48 @@ 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 (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]: + # 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): @@ -829,6 +1080,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. + 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) @@ -846,13 +1102,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, @@ -896,6 +1152,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`). + 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 @@ -921,6 +1187,138 @@ 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 + 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 + ) -> 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, + ) + ] + + 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 + 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. + 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) + request_id = cs.last_request_id + 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, + ) + ] + 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=RecoverBackend.BOOSTER, + subsume_indeterminate=True, + ) + ] + 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, + ) + request_id = cs.last_request_id + + # 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=RecoverBackend.KORE if is_kore else RecoverBackend.BOOSTER, + subsume_indeterminate=subsume_indeterminate, + ) + ] + # 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, + ) + ] + 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/integration/proof/test_imp.py b/pyk/src/tests/integration/proof/test_imp.py index 65be2ca7d4..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 @@ -902,6 +903,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 (HandoffFlavour.EXECUTE, HandoffFlavour.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, 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..6c104ad259 --- /dev/null +++ b/pyk/src/tests/unit/cterm/test_symbolic.py @@ -0,0 +1,76 @@ +from __future__ import annotations + +from typing import TYPE_CHECKING +from unittest.mock import Mock + +import pytest + +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, State, StuckResult + +if TYPE_CHECKING: + from pyk.cterm import CTerm + + +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_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) + + +_ABORT_SURFACE_DATA = ( + ('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_depth', _ABORT_SURFACE_DATA, ids=[d[0] for d in _ABORT_SURFACE_DATA] +) +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.depth == expected_depth + assert not result.vacuous + + +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/kcfg/test_explore.py b/pyk/src/tests/unit/kcfg/test_explore.py new file mode 100644 index 0000000000..dbab4b429c --- /dev/null +++ b/pyk/src/tests/unit/kcfg/test_explore.py @@ -0,0 +1,44 @@ +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, Step + +from ..test_kcfg import term + +if TYPE_CHECKING: + from pyk.kcfg.kcfg import KCFGExtendResult + + +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) + + +# 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, logs=()), + NoProgress, + ), + ('progress', CTermExecute(state=term(2), next_states=(), depth=3, vacuous=False, logs=()), Step), +) + + +@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/kcfg/test_store.py b/pyk/src/tests/unit/kcfg/test_store.py index 68f31f782c..4e3e3aa803 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, HandoffFlavour, 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,57 @@ 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=HandoffFlavour.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=HandoffFlavour.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 == [] diff --git a/pyk/src/tests/unit/kore/test_client.py b/pyk/src/tests/unit/kore/test_client.py index e93e4558c2..60aa9b89cb 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, @@ -381,6 +382,12 @@ 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', + ), ( 'default-error', JsonRpcError(message='foo', code=100, data={'bar': 1, 'baz': [2, 3]}), diff --git a/pyk/src/tests/unit/test_kcfg.py b/pyk/src/tests/unit/test_kcfg.py index f9dc69d1b0..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,6 +252,93 @@ def test_create_node() -> None: assert not cfg.is_stuck(new_node.id) +_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])), +) + + +@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_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)) + + # 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_equality_ignores_variants() -> None: + # 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_kore_handoffs_add_and_roundtrip() -> None: + 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=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 + restored = KCFG.from_dict(cfg.to_dict()) + assert restored.kore_handoffs == cfg.kore_handoffs + + 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 f28b292d21..5bef7e6c2a 100644 --- a/pyk/src/tests/unit/test_proof.py +++ b/pyk/src/tests/unit/test_proof.py @@ -1,17 +1,33 @@ from __future__ import annotations from typing import TYPE_CHECKING +from unittest.mock import Mock import pytest +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 +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, APRSummary +from pyk.proof.reachability import ( + APRFailureInfo, + APRProof, + APRProofExtendResult, + APRProofStuckResult, + APRProver, + APRSummary, + DecisiveInvalid, + Indeterminate, + RecoverTask, + Subsumed, + recover_task_for, + recovery_rung, +) from .kcfg.test_minimize import minimization_test_kcfg from .test_kcfg import node, node_dicts, term @@ -22,6 +38,9 @@ from pytest import TempPathFactory + from pyk.kcfg.kcfg import NodeAttr + from pyk.proof.reachability import SubsumptionCheck + @pytest.fixture(scope='function') def proof_dir(tmp_path_factory: TempPathFactory) -> Path: @@ -238,6 +257,128 @@ 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 + assert kcfg.is_stuck(n3.id) + + +_CSUBST_SENTINEL: Final = CSubst() + +_CHECK_SUBSUME_DATA: Final = ( + ('subsumed', _CSUBST_SENTINEL, False, Subsumed), + ('decisive-invalid', None, False, 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, + 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 + 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 _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) + + +_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], ...] = ( + # (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), + ('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_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 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 = [