Enable booster-only simplification via RPC flag, JSON logging on RPC, and standardize log forma#4919
Draft
ehildenb wants to merge 8 commits into
Draft
Enable booster-only simplification via RPC flag, JSON logging on RPC, and standardize log forma#4919ehildenb wants to merge 8 commits into
ehildenb wants to merge 8 commits into
Conversation
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 <noreply@anthropic.com>
Booster supports --log-format json but pyk never exposed it.
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.
…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.
Maps 12-char rule hash prefix -> source location string (file:line:col), parsed from allRules.txt in the kompiled definition directory.
…g formats PID now appears in every log line prefix, replacing the one-off os.getpid() calls added to the connect and proof-init messages.
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.
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.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Blocked on: runtimeverification/haskell-backend#4145
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: addJSONvariant toKoreExecLogFormatso 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.%(process)dto all log format strings for consistent PID tagging across the toolchain.pyk/ktool/kprint: addKPrint.all_rulescached property, mapping 12-char rule-hash prefixes to source locations parsed fromallRules.txt. Downstream consumers use this for getting rule source locations.pyk/ktool/kprint: add in-processKPrint(..., pyk_print=True)path, avoiding subprocess overhead when the KAST definition is already loaded. Without the option, current behavior remains default.pyk: surfacebooster-only-simplifyflag throughKoreClientandCTermSymbolic(blocked on haskell-backend adding that flag in Additional Kore logging, Claude enablement, boosteryOnly simplification flag per-rpc request haskell-backend#4145).