Enable booster-only simplification via RPC flag, JSON logging on RPC, and standardize log forma (#4919)

ehildenb · claude · web-flow · commit 79fb73503cad · 2026-05-28T12:28:53.000-06:00
~Blocked on: runtimeverification/haskell-backend#4145 ~Blocked on: #4902 This branch adds structured logging infrastructure to the pyk RPC layer to enable downstream log analysis tooling. The motivating use case is correlating simplification calls across worker processes, attributing them to source rules, and diagnosing fixability — none of which is possible without stable, parseable log output and hash-to-source mappings in pyk itself. Changes: - `pyk/kore/rpc`: add `JSON` variant to `KoreExecLogFormat` so execution logs are emitted as one JSON object per line rather than free-form text. The haskell backend already supports json logging. - `pyk/kore/rpc`: log the local port on connect, enabling correlation of log lines to specific worker processes. - All tools: add `%(process)d` to all log format strings for consistent PID tagging across the toolchain. - `pyk/ktool/kprint`: add `KPrint.all_rules` cached property, mapping 12-char rule-hash prefixes to source locations parsed from `allRules.txt`. Downstream consumers use this for getting rule source locations. - `pyk/ktool/kprint`: add in-process `KPrint(..., pyk_print=True)` path, avoiding subprocess overhead when the KAST definition is already loaded. Without the option, current behavior remains default. - `pyk`: surface `booster-only-simplify` flag through `KoreClient` and `CTermSymbolic` (blocked on haskell-backend adding that flag in runtimeverification/haskell-backend#4145). --------- Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
diff --git 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/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/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
@@ -44,6 +44,7 @@
 class KoreExecLogFormat(Enum):
     STANDARD = 'standard'
     ONELINE = 'oneline'
+    JSON = 'json'
 
 
 @final
@@ -119,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()
@@ -965,6 +967,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 +981,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,13 +995,15 @@ def implies(
         *,
         module_name: str | None = None,
         assume_defined: bool = False,
+        booster_only_simplify: bool | None = None,
     ) -> ImpliesResult:
         params = filter_none(
             {
                 'antecedent': self._state(antecedent),
                 'consequent': self._state(consequent),
                 'module': module_name,
                 'assume-defined': assume_defined,
+                'booster-only': booster_only_simplify,
             }
         )
 
@@ -1009,11 +1015,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,
             }
         )
 
diff --git 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
@@ -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/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
@@ -233,7 +249,9 @@ 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:
+    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,
