Additional Kore logging, Claude enablement, boosteryOnly simplification flag per-rpc request by ehildenb · Pull Request #4145 · runtimeverification/haskell-backend

ehildenb · 2026-05-24T21:41:54Z

I'm running a (so far successful) experiment downstream to enable Claude to debug "what work is the old Kore backend doing that the booster is not?" specifically for simplification queries. This PR contains the logging and infrastructure changes needed to enable Claude to, in the KEVM repo, mostly automatically debug this question about proofs, and then confirm that the proof is then working without any simplification calls to Kore using the added flag. In particular:

KoreCalls log level (-l KoreCalls): emit structured JSON entries ({tag, input, output}) on every Kore backend invocation — both kore-simplify and kore-execute-fallback — under the existing CtxProxy/CtxDetail context. Activating -l KoreCalls --log-format json produces a log stream from which input/output pairs where Kore changes the term can be extracted directly.
SimplifyKore log level (-l SimplifyKore): alias for the Kore-side filter request*>simplification*|function*,success. Also fixes DebugApplyEquation's JSON output to include {label, location, result} (equation name + source location) instead of just the result term, and adds DebugApplyEquation to the forwarded entry types for this level. Combining -l KoreCalls -l SimplifyKore gives full traceability from input state to applied equation.
boosterOnly RPC request flag: optional field on ExecuteRequest, SimplifyRequest, and ImpliesRequest. When set, the proxy skips the Kore pass entirely for any simplification on that request — useful for callers that have already established that Booster's answer is sufficient, or for regression testing Booster in isolation. Fallbacks for execute are still in place.
Peer-address logging on connect: jsonRpcServer now accepts an onConnect :: Text -> IO () callback fired once per accepted TCP connection. kore-rpc-booster logs the peer address at Proxy/Info, which lets operator logs be correlated with the pyk-side log when both are running with multiple processes and have interleaved output (which records the local port of the same socket).
Adds documentation related to how to submit bug reports as tests, and then upstream them into RPC regression tests. Used locally for testing/debugging, I'm hoping have this documentation present will keep Claude from guessing on how to do this in the future.
CLAUDE.md: adds a developer guide covering build commands, linting, test tiers, and architecture overview.

Validation:

Built and linked all affected executables (kore-rpc-types, kore-rpc-booster, kore-rpc, dev tools).
Confirmed -l KoreCalls is accepted at runtime (registered in allowedLogLevels).
Peer-address callback verified to compile without MonadLoggerIO constraints on the caller side (liftIO into the m callback from runGeneralTCPServer).
Tested with fragments of downstream and K and KEVM versions on fragments of their test-suites to check that we're getting the logging information we need out now, and can automatically debug simplify fallbacks with Claude skills.

…rence

…ion logging Adds instrumentation to answer: "What work is the old Kore backend doing that Booster cannot?" - Proxy.hs: emit structured JSON log entries on every Kore invocation - kore-simplify: {tag, input, output} under CtxProxy/CtxDetail - kore-execute-fallback: {tag, input, output, kore_reason} likewise - CLOptions.hs: add -l KoreCalls level that filters exactly these entries and register it in allowedLogLevels so -l KoreCalls is accepted at runtime Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

… conversion workflow Adds docs/submitting-test-cases.md: full guide for generating bug-report tarballs via kore-rpc-booster, replaying them with kore-rpc-client, and converting them into permanent runDirectoryTest-compatible tests. Covers the LLVM library rebuild workflow for new definitions. Updates CLAUDE.md Performance Testing section and the rpc-integration README to reference the new doc.

…ctured DebugApplyEquation output Three changes to enable post-hoc analysis of equations that Kore applies but Booster cannot: - CLOptions.hs: register 'SimplifyKore' as a named log-level alias for the context filter `request*>simplification*|function*,success`, so callers can use `-l SimplifyKore` instead of a raw context string. - Server.hs: add DebugApplyEquation to the Kore log entry types forwarded when SimplifyKore is active (previously only DebugAttemptEquation and DebugTerm were forwarded). - DebugEquation.hs: change DebugApplyEquation's oneLineJson to emit `{label, location, result}` instead of just the result term, so the equation name and source location appear in the combined JSON log. Together these allow `kore-rpc-booster -l KoreCalls -l SimplifyKore --log-format json` to produce logs from which downstream tools can identify exactly which equations Kore applies that Booster does not. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

…es requests Adds an optional `boosterOnly` field to `ExecuteRequest`, `SimplifyRequest`, and `ImpliesRequest`. When set, the proxy skips the Kore fallback/pass: - `handleSimplify`: returns Booster's result directly without forwarding to Kore. - `handleImplies`: returns Booster's error directly without falling back to Kore. - `simplifyExecuteState` / `simplifyExecResult`: thread `boosterOnly` through so post-execute simplification also respects the flag. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

…er: log peer address on connect Add an `onConnect :: Text -> IO ()` callback to `jsonRpcServer` that fires once per accepted TCP connection with the peer address string. `kore-rpc-booster` logs it at Proxy/Info so operator logs record which client (by ephemeral port) is talking to which server process. All other call sites pass a no-op. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

…ugApplyEquation entries Two fixes for the test-log-simplify-json golden-file comparison: - Server.hs: downgrade the "New connection from" log call from logMessage' (always-display) to logMessage (context-filtered). The peer address includes an ephemeral port that changes every connection, so always-displaying it breaks the deterministic diff. The message is still emitted; it just requires an explicit context filter to surface it. - simplify-log.txt.golden: add the new DebugApplyEquation entry produced when '-l Simplify' is active. The SimplifyKore commit added DebugApplyEquation to the set of kore log entry types forwarded by the proxy, and changed its oneLineJson to emit {label, location, result} rather than just the bare term. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

…efix Aligns with the naming convention of other files in docs/ (e.g. 2024-10-18-booster-description.md). Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

The KoreCalls log level (context filter request*,proxy,detail.) previously only covered kore-simplify and kore-execute-fallback. The implies and get-model handlers also call kore but emitted nothing under KoreCalls, making them invisible in kore-contribution triage. Four new CtxDetail log entries, all with the same {tag, ...fields} schema as the existing entries: kore-implies — default implies path (assumeDefined=False), always sent to kore kore-implies-fallback — booster-first path where booster errored and kore handled the check kore-get-model-fallback — booster returned an error, kore took over kore-get-model-recheck — booster returned Unknown, kore re-checked Each entry logs antecedent/consequent (implies) or state (get-model) as input, plus valid/satisfiable from the kore result when successful. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

jberthold · 2026-05-26T08:30:41Z

+## What is a bug-report tarball?
+
+`kore-rpc-booster` can capture a self-contained reproduction of any request sequence
+as a **bug-report tarball**: a `.tar.gz` file containing the compiled `.kore` definition,


(minor) Is it actually compressed, or just a *.tar file ?

Suggested change

as a **bug-report tarball**: a `.tar.gz` file containing the compiled `.kore` definition,

as a **bug-report tarball**: a `.tar` file containing the compiled `.kore` definition,

The files are .tar.gz — the code in kore/src/Kore/BugReport.hs explicitly gzip-compresses the archive before writing: ByteString.Lazy.writeFile filename . GZip.compress . Tar.write. The docs and the script are correct as-is. No change needed here.

jberthold · 2026-05-26T08:39:37Z

+The `kore-rpc-client run-tarball` subcommand starts a server, replays all requests, and
+prints any mismatches:
+
+```sh
+cabal build kore-rpc-client kore-rpc-booster
+
+kore-rpc-client run-tarball my-issue.tar.gz
+```
+
+For the LLVM library, either set `LLVM_LIB` (path to a compatible pre-built `.so`) or
+`PLUGIN_DIR` (path to `blockchain-k-plugin`, used to compile the LLVM backend on the
+fly). See `scripts/run-with-tarball.sh` for the full set of environment variables.


The kore-rpc-client does not start the server, this is done by the helper script.

Suggested change

The `kore-rpc-client run-tarball` subcommand starts a server, replays all requests, and

prints any mismatches:

```sh

cabal build kore-rpc-client kore-rpc-booster

kore-rpc-client run-tarball my-issue.tar.gz

```

For the LLVM library, either set `LLVM_LIB` (path to a compatible pre-built `.so`) or

`PLUGIN_DIR` (path to `blockchain-k-plugin`, used to compile the LLVM backend on the

fly). See `scripts/run-with-tarball.sh` for the full set of environment variables.

The `kore-rpc-client run-tarball` subcommand starts a server, replays all requests, and

prints any mismatches:

```sh

cabal build kore-rpc-client kore-rpc-booster

scripts/run-with-tarball.sh my-issue.tar.gz

For the LLVM library, either set LLVM_LIB (path to a compatible pre-built .so) or
PLUGIN_DIR (path to blockchain-k-plugin, used to compile the LLVM backend on the
fly). See scripts/run-with-tarball.sh for the full set of environment variables.

The script is a bit older, but AFAICT the LLVM compilation script is still valid.

Fixed in e66c26a. The section now correctly describes scripts/run-with-tarball.sh as the all-in-one script (starts server + replays), and notes that kore-rpc-client run-tarball only connects to an already-running server.

jberthold · 2026-05-26T08:45:27Z

                    | Unknown <- res.satisfiable -> do
                        Booster.Log.withContext CtxProxy $
                            Booster.Log.withContext CtxAbort $
                                Booster.Log.logMessage $
                                    Text.pack "Re-checking a get-model result Unknown"
-                        r@(kResult, _) <- Stats.timed $ kore req
+                        (kResult, kTime) <- Stats.timed $ kore req
                        Booster.Log.withContext CtxProxy $
                            Booster.Log.withContext CtxAbort $
                                Booster.Log.logMessage $
                                    "Double-check returned " <> toStrict (encodeToLazyText kResult)
-                        pure r
+                        Booster.Log.withContext CtxProxy $
+                            Booster.Log.withContext CtxDetail $
+                                Booster.Log.logMessage $
+                                    WithJsonMessage
+                                        ( object $
+                                            [ "tag" .= ("kore-get-model-recheck" :: Text)


As shown by this sequence of log statements, the CtxProxy, CtxAbort markers were also used to log information about the fall-backs that aren't actual "Aborts". This was helpful (when the messages do not get too long) for a quick diagnosis by running with -l Aborts. Consider reworking the contexts for these?

Fixed in 168b034. The filter is now request*,proxy>detail. (using > = ThenChild / subsequence) so it captures detail entries both with and without an intermediate abort context item. Fallback entries (kore-execute-fallback, kore-implies-fallback, kore-get-model-fallback, kore-get-model-recheck) now use withContexts [CtxProxy, CtxAbort, CtxDetail] to emit context [request, proxy, abort, detail].

jberthold · 2026-05-26T08:48:34Z

+                                    Booster.Log.withContext CtxProxy $
+                                        Booster.Log.withContext CtxDetail $


Maybe CtxProxy, CtxAbort, CtxDetail here? (Or rework the other locations, as mentioned)

Fixed in the same commit (168b034). A new filter request*,proxy>abort,detail. was added to the Aborts level, which matches the [request, proxy, abort, detail] context path used by all fallback kore-call entries. Non-fallback entries (kore-simplify, kore-implies) keep [CtxProxy, CtxDetail] and are only captured by KoreCalls.

jberthold · 2026-05-26T08:53:18Z

+    oneLineJson (DebugApplyEquation equation result) =
+        JSON.object
+            [ "label" JSON..= ruleLabel equation
+            , "location" JSON..= fmap (renderDefault . pretty) (srcLoc equation)
+            , "result"
+                JSON..= (JSON.toJSON $ Kore.Syntax.Json.fromTermLike . getRewritingTerm $ toTermLike result)
+            ]


I see how this might be helpful but the equation's unique ID will usually be in the context of any message logged using this helper.

Fixed in cbf75c6. The label field is now omitted entirely when ruleLabel returns Nothing; it is only included when a human-readable klabel is available. The location and result fields are always present.

jberthold · 2026-05-26T08:55:44Z

+
+```sh
+# Standard build (with optimisations)
+stack build all


Maybe add --copy-bins, many tools/scripts assume the results in .build/kore/bin are up to date.
Also always run the tests when building.

Suggested change

stack build all

stack build --test --copy-bins

I usually have this with an additional --file-watch running in a shell that I can see.

Done in 85f7bdb. Updated the CLAUDE.md build command to stack build --test --copy-bins all with a note that --copy-bins puts executables on $PATH.

jberthold · 2026-05-26T08:59:43Z

+### 4. Booster RPC integration tests (~minutes, needs K binaries)
+```sh
+# From inside the integration nix shell (see below):
+cd booster/test/rpc-integration && ./runDirectoryTest test-<name>
+```


There are a number of tests that use specific configurations and server options etc.
The script scripts/booster-integration-test.sh knows all of them by name and how they are supposed to be executed. It has to run within the nix develop .#cabal shell.
This script also runs the llvm-integration test, which needs a K framework.

Done in 85f7bdb. Added scripts/booster-integration-tests.sh as the full-suite runner alongside the existing single-directory runDirectoryTest.sh example.

jberthold · 2026-05-26T09:06:26Z

+  , ...
+  }
+```
+


Suggested change

This configuration is controlled by server options, see `booster/tools/booster/Server.hs:clProxyOptionsParser`.

Done in 85f7bdb. Added a pointer to clProxyOptionsParser in booster/tools/booster/Server.hs directly below the ProxyConfig record documentation.

`kore-rpc-client run-tarball` does not start a server; it connects to an already-running one. `scripts/run-with-tarball.sh` is the all-in-one script that starts the server and then replays the tarball requests. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

All kore-call entries that represent a fallback (kore-execute-fallback, kore-implies-fallback, kore-get-model-fallback, kore-get-model-recheck) now use withContexts [CtxProxy, CtxAbort, CtxDetail] so that their context path is [request, "proxy", "abort", "detail"]. This makes them visible under both: -l KoreCalls (filter widened from proxy,detail. to proxy>detail. to match both with and without the intermediate abort) -l Aborts (new filter request*,proxy>abort,detail. added) Non-fallback entries (kore-simplify, kore-implies) keep CtxProxy,CtxDetail and are only captured by KoreCalls. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

When an equation has no klabel (ruleLabel = Nothing), the previous code emitted "label": null in the JSON. Omit the field entirely when absent so consumers don't need to handle null; include it only when a human-readable label is available. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

…nter - Build command: add --test --copy-bins to stack build so binaries land on PATH immediately (comment 6) - RPC integration tests: mention scripts/booster-integration-tests.sh as the full-suite runner alongside the single-directory form (comment 7) - ProxyConfig: add pointer to clProxyOptionsParser in Server.hs where the CLI flags for those fields are defined (comment 8) Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

ehildenb and others added 7 commits May 24, 2026 21:50

CLAUDE.md: add developer guide with build/lint/test/architecture refe…

1299392

…rence

Format with fourmolu

5d7a021

ehildenb force-pushed the kore-logging-additions branch from bffbc41 to 5d7a021 Compare May 24, 2026 21:55

ehildenb requested a review from jberthold May 25, 2026 12:50

ehildenb marked this pull request as ready for review May 25, 2026 12:50

docs, CLAUDE.md, README: rename submitting-test-cases.md with date pr…

2250a44

…efix Aligns with the naming convention of other files in docs/ (e.g. 2024-10-18-booster-description.md). Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

ehildenb mentioned this pull request May 25, 2026

Enable booster-only simplification via RPC flag, JSON logging on RPC, and standardize log forma runtimeverification/k#4919

Draft

jberthold approved these changes May 26, 2026

View reviewed changes

ehildenb and others added 4 commits May 26, 2026 16:50

ehildenb added the automerge label May 26, 2026

	as a bug-report tarball: a `.tar.gz` file containing the compiled `.kore` definition,
	as a bug-report tarball: a `.tar` file containing the compiled `.kore` definition,

		Booster.Log.withContext CtxProxy $
		Booster.Log.withContext CtxDetail $


	This configuration is controlled by server options, see `booster/tools/booster/Server.hs:clProxyOptionsParser`.

Conversation

ehildenb commented May 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

ehildenb commented May 24, 2026 •

edited

Loading