From 1f1848055574939a80174e74e627a243e3693f62 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 23 May 2026 22:22:42 +0000 Subject: [PATCH 1/8] pyk: surface booster-only simplify flag to CTermSymbolic and KoreClient Adds `booster_only_simplify` to `KoreClient.execute`, `.simplify`, and `.implies` (mapped to the `booster-only` JSON-RPC field), and surfaces it at the `CTermSymbolic` level as a class-level default with per-call override on `execute`, `simplify`, `kast_simplify`, `implies`, and `assume_defined` (the last always defaults to False, independent of the class setting). Co-Authored-By: Claude Sonnet 4.6 --- pyk/src/pyk/cterm/symbolic.py | 56 +++++++++++++++++++++++++++++------ pyk/src/pyk/kore/rpc.py | 6 ++++ 2 files changed, 53 insertions(+), 9 deletions(-) diff --git a/pyk/src/pyk/cterm/symbolic.py b/pyk/src/pyk/cterm/symbolic.py index cef9c9f8db..f7c20cca79 100644 --- a/pyk/src/pyk/cterm/symbolic.py +++ b/pyk/src/pyk/cterm/symbolic.py @@ -73,6 +73,7 @@ class CTermSymbolic: _definition: KDefinition _log_succ_rewrites: bool _log_fail_rewrites: bool + _booster_only_simplify: bool def __init__( self, @@ -81,11 +82,13 @@ def __init__( *, log_succ_rewrites: bool = True, log_fail_rewrites: bool = False, + booster_only_simplify: bool = False, ): self._kore_client = kore_client self._definition = definition self._log_succ_rewrites = log_succ_rewrites self._log_fail_rewrites = log_fail_rewrites + self._booster_only_simplify = booster_only_simplify def kast_to_kore(self, kinner: KInner) -> Pattern: return kast_to_kore(self._definition, kinner, sort=GENERATED_TOP_CELL) @@ -100,6 +103,7 @@ def execute( cut_point_rules: Iterable[str] | None = None, terminal_rules: Iterable[str] | None = None, module_name: str | None = None, + booster_only_simplify: bool | None = None, ) -> CTermExecute: _LOGGER.debug(f'Executing: {cterm}') @@ -113,6 +117,9 @@ def execute( module_name=module_name, log_successful_rewrites=self._log_succ_rewrites, log_failed_rewrites=self._log_succ_rewrites and self._log_fail_rewrites, + booster_only_simplify=( + booster_only_simplify if booster_only_simplify is not None else self._booster_only_simplify + ), ) except SmtSolverError as err: raise self._smt_solver_error(err) from err @@ -143,16 +150,28 @@ def execute( logs=response.logs, ) - def simplify(self, cterm: CTerm, module_name: str | None = None) -> tuple[CTerm, tuple[LogEntry, ...]]: + def simplify( + self, cterm: CTerm, module_name: str | None = None, booster_only_simplify: bool | None = None + ) -> tuple[CTerm, tuple[LogEntry, ...]]: _LOGGER.debug(f'Simplifying: {cterm}') - kast_simplified, logs = self.kast_simplify(cterm.kast, module_name=module_name) + kast_simplified, logs = self.kast_simplify( + cterm.kast, module_name=module_name, booster_only_simplify=booster_only_simplify + ) return CTerm.from_kast(kast_simplified), logs - def kast_simplify(self, kast: KInner, module_name: str | None = None) -> tuple[KInner, tuple[LogEntry, ...]]: + def kast_simplify( + self, kast: KInner, module_name: str | None = None, booster_only_simplify: bool | None = None + ) -> tuple[KInner, tuple[LogEntry, ...]]: _LOGGER.debug(f'Simplifying: {kast}') kore = self.kast_to_kore(kast) try: - kore_simplified, logs = self._kore_client.simplify(kore, module_name=module_name) + kore_simplified, logs = self._kore_client.simplify( + kore, + module_name=module_name, + booster_only_simplify=( + booster_only_simplify if booster_only_simplify is not None else self._booster_only_simplify + ), + ) except SmtSolverError as err: raise self._smt_solver_error(err) from err @@ -194,6 +213,7 @@ def implies( failure_reason: bool = False, module_name: str | None = None, assume_defined: bool = False, + booster_only_simplify: bool | None = None, ) -> CTermImplies: _LOGGER.debug(f'Checking implication: {antecedent} #Implies {consequent}') _consequent = consequent.kast @@ -211,7 +231,13 @@ def implies( consequent_kore = self.kast_to_kore(_consequent) try: result = self._kore_client.implies( - antecedent_kore, consequent_kore, module_name=module_name, assume_defined=assume_defined + antecedent_kore, + consequent_kore, + module_name=module_name, + assume_defined=assume_defined, + booster_only_simplify=( + booster_only_simplify if booster_only_simplify is not None else self._booster_only_simplify + ), ) except SmtSolverError as err: raise self._smt_solver_error(err) from err @@ -231,6 +257,7 @@ def implies( failure_reason=False, module_name=module_name, assume_defined=assume_defined, + booster_only_simplify=booster_only_simplify, ) config_match = _config_match.csubst if config_match is None: @@ -269,11 +296,17 @@ def implies( csubst = CSubst.from_pred(ml_subst_pred) return CTermImplies(csubst, (), None, result.logs) - def assume_defined(self, cterm: CTerm, module_name: str | None = None) -> CTerm: + def assume_defined( + self, cterm: CTerm, module_name: str | None = None, booster_only_simplify: bool = False + ) -> CTerm: _LOGGER.debug(f'Computing definedness condition for: {cterm}') - cterm_simplified, logs = self.simplify(cterm, module_name=module_name) + cterm_simplified, logs = self.simplify( + cterm, module_name=module_name, booster_only_simplify=booster_only_simplify + ) kast = KApply(KLabel('#Ceil', [GENERATED_TOP_CELL, GENERATED_TOP_CELL]), [cterm_simplified.config]) - kast_simplified, logs = self.kast_simplify(kast, module_name=module_name) + kast_simplified, logs = self.kast_simplify( + kast, module_name=module_name, booster_only_simplify=booster_only_simplify + ) _LOGGER.debug(f'Definedness condition computed: {kast_simplified}') return cterm.add_constraint(kast_simplified) @@ -305,6 +338,7 @@ def cterm_symbolic( log_axioms_file: Path | None = None, log_succ_rewrites: bool = True, log_fail_rewrites: bool = False, + booster_only_simplify: bool = False, start_server: bool = True, fallback_on: Iterable[FallbackReason] | None = None, interim_simplification: int | None = None, @@ -333,7 +367,11 @@ def cterm_symbolic( ) as server: with KoreClient('localhost', server.port, bug_report=bug_report, bug_report_id=id) as client: yield CTermSymbolic( - client, definition, log_succ_rewrites=log_succ_rewrites, log_fail_rewrites=log_fail_rewrites + client, + definition, + log_succ_rewrites=log_succ_rewrites, + log_fail_rewrites=log_fail_rewrites, + booster_only_simplify=booster_only_simplify, ) else: if port is None: diff --git a/pyk/src/pyk/kore/rpc.py b/pyk/src/pyk/kore/rpc.py index 77ef641a8f..973e9c67d1 100644 --- a/pyk/src/pyk/kore/rpc.py +++ b/pyk/src/pyk/kore/rpc.py @@ -965,6 +965,7 @@ def execute( module_name: str | None = None, log_successful_rewrites: bool | None = None, log_failed_rewrites: bool | None = None, + booster_only_simplify: bool | None = None, ) -> ExecuteResult: params = filter_none( { @@ -978,6 +979,7 @@ def execute( 'state': self._state(pattern), 'log-successful-rewrites': log_successful_rewrites, 'log-failed-rewrites': log_failed_rewrites, + 'booster-only': booster_only_simplify, } ) @@ -991,6 +993,7 @@ def implies( *, module_name: str | None = None, assume_defined: bool = False, + booster_only_simplify: bool | None = None, ) -> ImpliesResult: params = filter_none( { @@ -998,6 +1001,7 @@ def implies( 'consequent': self._state(consequent), 'module': module_name, 'assume-defined': assume_defined, + 'booster-only': booster_only_simplify, } ) @@ -1009,11 +1013,13 @@ def simplify( pattern: Pattern, *, module_name: str | None = None, + booster_only_simplify: bool | None = None, ) -> tuple[Pattern, tuple[LogEntry, ...]]: params = filter_none( { 'state': self._state(pattern), 'module': module_name, + 'booster-only': booster_only_simplify, } ) From bd18ae06192cdcfd52b198e13212daf947531976 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 23 May 2026 22:59:13 +0000 Subject: [PATCH 2/8] pyk/kore/rpc: add JSON variant to KoreExecLogFormat Booster supports --log-format json but pyk never exposed it. --- pyk/src/pyk/kore/rpc.py | 1 + 1 file changed, 1 insertion(+) diff --git a/pyk/src/pyk/kore/rpc.py b/pyk/src/pyk/kore/rpc.py index 973e9c67d1..d44e8eef58 100644 --- a/pyk/src/pyk/kore/rpc.py +++ b/pyk/src/pyk/kore/rpc.py @@ -44,6 +44,7 @@ class KoreExecLogFormat(Enum): STANDARD = 'standard' ONELINE = 'oneline' + JSON = 'json' @final From b11c07d69732d9f3f2318f5a38aa5c0a5ee8536e Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sun, 24 May 2026 03:57:27 +0000 Subject: [PATCH 3/8] pyk/kore/rpc: log local port on connect to enable worker correlation When the booster adds peer-address logging on connection accept, the local port logged here can be matched against it to identify which worker thread a KoreClient is talking to. --- pyk/src/pyk/kore/rpc.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/pyk/src/pyk/kore/rpc.py b/pyk/src/pyk/kore/rpc.py index d44e8eef58..dff11c23b4 100644 --- a/pyk/src/pyk/kore/rpc.py +++ b/pyk/src/pyk/kore/rpc.py @@ -120,7 +120,8 @@ def _create_connection(host: str, port: int, timeout: int | None) -> socket.sock try: sock = socket.socket(socket.AF_INET, socket.SOCK_STREAM) sock.connect((host, port)) - _LOGGER.info(f'Connected to host: {host}:{port}') + local_port = sock.getsockname()[1] + _LOGGER.info(f'Connected to host: {host}:{port} (local port: {local_port})') return sock except ConnectionRefusedError: sock.close() From 380a13c9d97625e616927406074e3ad3c433be08 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sun, 24 May 2026 05:20:49 +0000 Subject: [PATCH 4/8] pyk/kore/rpc, pyk/proof/proof: add pid to connect and proof-init log lines Correlate claim name with kore RPC worker: grep pyk.log for matching pids in "Initializing proof: CLAIM (pid: N)" and "Connected to host:PORT (local port: X, pid: N)" lines. --- pyk/src/pyk/kore/rpc.py | 2 +- pyk/src/pyk/proof/proof.py | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/pyk/src/pyk/kore/rpc.py b/pyk/src/pyk/kore/rpc.py index dff11c23b4..4926018f6f 100644 --- a/pyk/src/pyk/kore/rpc.py +++ b/pyk/src/pyk/kore/rpc.py @@ -121,7 +121,7 @@ def _create_connection(host: str, port: int, timeout: int | None) -> socket.sock sock = socket.socket(socket.AF_INET, socket.SOCK_STREAM) sock.connect((host, port)) local_port = sock.getsockname()[1] - _LOGGER.info(f'Connected to host: {host}:{port} (local port: {local_port})') + _LOGGER.info(f'Connected to host: {host}:{port} (local port: {local_port}, pid: {os.getpid()})') return sock except ConnectionRefusedError: sock.close() diff --git a/pyk/src/pyk/proof/proof.py b/pyk/src/pyk/proof/proof.py index 0d1eef04d2..f9b0614488 100644 --- a/pyk/src/pyk/proof/proof.py +++ b/pyk/src/pyk/proof/proof.py @@ -2,6 +2,7 @@ import json import logging +import os from abc import ABC, abstractmethod from concurrent.futures import ThreadPoolExecutor, wait from dataclasses import dataclass @@ -520,7 +521,7 @@ def advance_proof( maintenance_rate: Number of iterations between proof maintenance (writing to disk and executing callback). """ iterations = 0 - _LOGGER.info(f'Initializing proof: {proof.id}') + _LOGGER.info(f'Initializing proof: {proof.id} (pid: {os.getpid()})') self.init_proof(proof) while True: steps = list(proof.get_steps()) From c30a8aa004922cd7d89f3477177857c2f21361b9 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sun, 24 May 2026 17:11:39 +0000 Subject: [PATCH 5/8] pyk/ktool/kprint: add all_rules cached_property to KPrint Maps 12-char rule hash prefix -> source location string (file:line:col), parsed from allRules.txt in the kompiled definition directory. --- pyk/src/pyk/ktool/kprint.py | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/pyk/src/pyk/ktool/kprint.py b/pyk/src/pyk/ktool/kprint.py index 4e1c9ccfda..77f253fea9 100644 --- a/pyk/src/pyk/ktool/kprint.py +++ b/pyk/src/pyk/ktool/kprint.py @@ -219,6 +219,22 @@ def _temp_file(self, prefix: str | None = None, suffix: str | None = None) -> It def definition(self) -> KDefinition: return read_kast_definition(self.definition_dir / 'compiled.json') + @cached_property + def all_rules(self) -> dict[str, str]: + """Map from 12-char rule hash prefix to source location (file:line:col). + + Parsed from allRules.txt in the kompiled definition directory. + Keyed by the first 12 hex characters of each rule's SHA-256 hash. + """ + rules: dict[str, str] = {} + for line in (self.definition_dir / 'allRules.txt').read_text().splitlines(): + line = line.strip() + if not line: + continue + full_hash, _, location = line.partition(' ') + rules[full_hash[:12]] = location + return rules + @property def definition_hash(self) -> str: return self.definition.hash From 6db29fa18d4f35bc93c416767e83c631aeeebeaf Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sun, 24 May 2026 17:20:00 +0000 Subject: [PATCH 6/8] pyk/cli/utils, kdist/utils, kore_exec_covr: add %(process)d to all log formats PID now appears in every log line prefix, replacing the one-off os.getpid() calls added to the connect and proof-init messages. --- pyk/src/pyk/cli/utils.py | 2 +- pyk/src/pyk/kdist/utils.py | 2 +- pyk/src/pyk/kore/rpc.py | 2 +- pyk/src/pyk/kore_exec_covr/__main__.py | 2 +- pyk/src/pyk/kore_exec_covr/kore_exec_covr.py | 2 +- pyk/src/pyk/proof/proof.py | 3 +-- 6 files changed, 6 insertions(+), 7 deletions(-) diff --git a/pyk/src/pyk/cli/utils.py b/pyk/src/pyk/cli/utils.py index c98320fdd6..bc7435bcce 100644 --- a/pyk/src/pyk/cli/utils.py +++ b/pyk/src/pyk/cli/utils.py @@ -16,7 +16,7 @@ T1 = TypeVar('T1') T2 = TypeVar('T2') -LOG_FORMAT: Final = '%(levelname)s %(asctime)s %(name)s - %(message)s' +LOG_FORMAT: Final = '%(levelname)s %(asctime)s %(name)s [%(process)d] - %(message)s' def loglevel(args: Namespace) -> int: diff --git a/pyk/src/pyk/kdist/utils.py b/pyk/src/pyk/kdist/utils.py index 38c275f131..164cc13979 100644 --- a/pyk/src/pyk/kdist/utils.py +++ b/pyk/src/pyk/kdist/utils.py @@ -13,7 +13,7 @@ from typing import Any, Final -LOG_FORMAT: Final = '%(levelname)s %(asctime)s %(name)s - %(message)s' +LOG_FORMAT: Final = '%(levelname)s %(asctime)s %(name)s [%(process)d] - %(message)s' def package_path(obj: Any) -> Path: diff --git a/pyk/src/pyk/kore/rpc.py b/pyk/src/pyk/kore/rpc.py index 4926018f6f..dff11c23b4 100644 --- a/pyk/src/pyk/kore/rpc.py +++ b/pyk/src/pyk/kore/rpc.py @@ -121,7 +121,7 @@ def _create_connection(host: str, port: int, timeout: int | None) -> socket.sock sock = socket.socket(socket.AF_INET, socket.SOCK_STREAM) sock.connect((host, port)) local_port = sock.getsockname()[1] - _LOGGER.info(f'Connected to host: {host}:{port} (local port: {local_port}, pid: {os.getpid()})') + _LOGGER.info(f'Connected to host: {host}:{port} (local port: {local_port})') return sock except ConnectionRefusedError: sock.close() diff --git a/pyk/src/pyk/kore_exec_covr/__main__.py b/pyk/src/pyk/kore_exec_covr/__main__.py index d0957da33a..ccf76b8646 100644 --- a/pyk/src/pyk/kore_exec_covr/__main__.py +++ b/pyk/src/pyk/kore_exec_covr/__main__.py @@ -16,7 +16,7 @@ from typing import Final -_LOG_FORMAT: Final = '%(levelname)s %(name)s - %(message)s' +_LOG_FORMAT: Final = '%(levelname)s %(name)s [%(process)d] - %(message)s' def do_analyze(definition_dir: Path, input_file: Path) -> None: diff --git a/pyk/src/pyk/kore_exec_covr/kore_exec_covr.py b/pyk/src/pyk/kore_exec_covr/kore_exec_covr.py index 4792514d18..25fc163e6f 100644 --- a/pyk/src/pyk/kore_exec_covr/kore_exec_covr.py +++ b/pyk/src/pyk/kore_exec_covr/kore_exec_covr.py @@ -15,7 +15,7 @@ from ..kast.outer import KDefinition, KRule -_LOG_FORMAT: Final = '%(levelname)s %(name)s - %(message)s' +_LOG_FORMAT: Final = '%(levelname)s %(name)s [%(process)d] - %(message)s' _LOGGER: Final = logging.getLogger(__name__) _HASKELL_LOG_ENTRY_REGEXP: Final = re.compile(r'(kore-exec|kore-rpc): \[\d*\] Debug \(([a-zA-Z]*)\):(.*)') diff --git a/pyk/src/pyk/proof/proof.py b/pyk/src/pyk/proof/proof.py index f9b0614488..0d1eef04d2 100644 --- a/pyk/src/pyk/proof/proof.py +++ b/pyk/src/pyk/proof/proof.py @@ -2,7 +2,6 @@ import json import logging -import os from abc import ABC, abstractmethod from concurrent.futures import ThreadPoolExecutor, wait from dataclasses import dataclass @@ -521,7 +520,7 @@ def advance_proof( maintenance_rate: Number of iterations between proof maintenance (writing to disk and executing callback). """ iterations = 0 - _LOGGER.info(f'Initializing proof: {proof.id} (pid: {os.getpid()})') + _LOGGER.info(f'Initializing proof: {proof.id}') self.init_proof(proof) while True: steps = list(proof.get_steps()) From afe8a9628d4c960c5a61e38dcf41438481bbf582 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sun, 24 May 2026 18:45:49 +0000 Subject: [PATCH 7/8] pyk/ktool/kprint: replace kore_to_pretty subprocess with in-process path kore_to_pretty previously called kast --input kore --output pretty. The kore_to_kast + pretty_print path is always at least as fast: the Python converter handles EVar/DV/ML constructs in-process, and the existing kore-print fallback in kore_to_kast covers polymorphic App operators. --- pyk/src/pyk/ktool/kprint.py | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/pyk/src/pyk/ktool/kprint.py b/pyk/src/pyk/ktool/kprint.py index 77f253fea9..ef5034ac4c 100644 --- a/pyk/src/pyk/ktool/kprint.py +++ b/pyk/src/pyk/ktool/kprint.py @@ -250,12 +250,7 @@ def parse_token(self, ktoken: KToken, *, as_rule: bool = False) -> KInner: return KInner.from_dict(kast_term(json.loads(proc_res.stdout))) def kore_to_pretty(self, pattern: Pattern) -> str: - proc_res = self._expression_kast( - pattern.text, - input=KAstInput.KORE, - output=KAstOutput.PRETTY, - ) - return proc_res.stdout + return self.pretty_print(self.kore_to_kast(pattern)) def kore_to_kast(self, kore: Pattern) -> KInner: try: From 2616a3ed1a64112cb8703a658ca86606bafeb2b8 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sun, 24 May 2026 18:46:37 +0000 Subject: [PATCH 8/8] pyk/ktool/kprint: restore kore_to_pretty subprocess, add pyk_print flag The two paths don't always agree, so the original kast subprocess behavior is kept as the default. Pass pyk_print=True to use the in-process kore_to_kast + pretty_print path instead. --- pyk/src/pyk/ktool/kprint.py | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/pyk/src/pyk/ktool/kprint.py b/pyk/src/pyk/ktool/kprint.py index ef5034ac4c..d4b48ecf54 100644 --- a/pyk/src/pyk/ktool/kprint.py +++ b/pyk/src/pyk/ktool/kprint.py @@ -249,8 +249,15 @@ def parse_token(self, ktoken: KToken, *, as_rule: bool = False) -> KInner: ) return KInner.from_dict(kast_term(json.loads(proc_res.stdout))) - def kore_to_pretty(self, pattern: Pattern) -> str: - return self.pretty_print(self.kore_to_kast(pattern)) + def kore_to_pretty(self, pattern: Pattern, *, pyk_print: bool = False) -> str: + if pyk_print: + return self.pretty_print(self.kore_to_kast(pattern)) + proc_res = self._expression_kast( + pattern.text, + input=KAstInput.KORE, + output=KAstOutput.PRETTY, + ) + return proc_res.stdout def kore_to_kast(self, kore: Pattern) -> KInner: try: