Skip to content

Commit dc48de7

Browse files
ehildenbclaudegithub-actions
authored
Additional Kore logging, Claude enablement, boosteryOnly simplification flag per-rpc request (#4145)
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. --------- Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com> Co-authored-by: github-actions <github-actions@github.com>
1 parent 00479fb commit dc48de7

13 files changed

Lines changed: 569 additions & 67 deletions

File tree

‎CLAUDE.md‎

Lines changed: 210 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,210 @@
1+
# haskell-backend — Developer Guide for Claude
2+
3+
## What This Is
4+
5+
A symbolic execution engine for the [K Framework](https://github.com/runtimeverification/k).
6+
Programs in K-specified languages are compiled to `Kore` (an intermediate representation),
7+
and this backend executes/proves them symbolically via a JSON-RPC server.
8+
9+
The primary binary is `kore-rpc-booster` — a two-engine proxy that routes requests
10+
through a fast engine (Booster) first and falls back to the old engine (Kore) when needed.
11+
12+
---
13+
14+
## Repository Layout
15+
16+
```
17+
kore/ Old Haskell backend — complete but slow; three entrypoints:
18+
kore-exec (deprecated), kore-repl, kore-rpc (legacy)
19+
booster/ Fast rewrite engine + proxy server
20+
library/Booster/ Core library: Pattern/, SMT/, LLVM/, JsonRpc/, …
21+
tools/booster/ kore-rpc-booster server (Proxy.hs is the key file)
22+
tools/rpc-client/ kore-rpc-client (testing/scripted RPC calls)
23+
unit-tests/ Tasty unit tests (tasty-discover)
24+
test/ Integration tests: llvm-integration/, rpc-integration/, …
25+
kore-rpc-types/ Shared JSON-RPC type definitions
26+
dev-tools/ Utilities: kore-parser, pretty, count-aborts, process-logs, …
27+
test/ 70+ make-driven integration test directories (require K framework)
28+
docs/ Architecture docs; 2024-10-18-booster-description.md is essential
29+
scripts/ Performance and analysis scripts
30+
deps/k_release Pins the required K framework version
31+
```
32+
33+
---
34+
35+
## Building
36+
37+
```sh
38+
# Standard build (with optimisations); --copy-bins puts executables on $PATH
39+
stack build --test --copy-bins all
40+
# or
41+
cabal build all
42+
43+
# Fast dev build (no optimisations — slower runtime, faster compile)
44+
stack build --fast all
45+
cabal build -O0 all
46+
47+
# Via Nix dev shell
48+
nix develop .#cabal --command cabal build all
49+
```
50+
51+
`stack.yaml` is the authoritative package resolver (LTS 22.23, GHC 9.6.5).
52+
`cabal.project.freeze` pins versions for reproducible non-Nix builds.
53+
Run `hpack` inside `booster/` if you edit `package.yaml` before cabal sees changes.
54+
55+
---
56+
57+
## Linting and Formatting
58+
59+
The CI enforces both — fix them before pushing.
60+
Fourmolu must pass on **every commit**, not just the final one.
61+
62+
```sh
63+
# Format all Haskell files (fourmolu)
64+
nix develop .#style --command scripts/fourmolu.sh
65+
66+
# Format a single file interactively
67+
nix develop .#style
68+
fourmolu path/to/Foo.hs
69+
70+
# HLint (configured via .hlint.yaml)
71+
hlint .
72+
```
73+
74+
Config files: `fourmolu.yaml` (100-col limit, 4-space indent, leading commas),
75+
`.hlint.yaml` (many suppressions — read before adding ignores).
76+
77+
---
78+
79+
## Running Tests (Shortest to Longest)
80+
81+
### 1. Booster unit tests (~5–30 s)
82+
```sh
83+
stack test hs-backend-booster:unit-tests
84+
# or
85+
cabal test unit-tests
86+
```
87+
Pure Haskell, no external dependencies. Source: `booster/unit-tests/`.
88+
89+
### 2. Kore unit tests (~1–5 min)
90+
```sh
91+
stack test kore
92+
# or
93+
cabal test kore-test
94+
```
95+
Source: `kore/test/`. The Makefile target is `make test-kore`.
96+
97+
### 3. LLVM integration tests (~minutes, needs LLVM shared lib)
98+
```sh
99+
cabal test llvm-integration
100+
```
101+
102+
### 4. Booster RPC integration tests (~minutes, needs K binaries)
103+
```sh
104+
# Run the full booster integration test suite:
105+
scripts/booster-integration-tests.sh
106+
107+
# Or run a single directory from inside the integration nix shell (see below):
108+
cd booster/test/rpc-integration && ./runDirectoryTest.sh test-<name>
109+
```
110+
111+
### 5. Full K integration tests (~many minutes, needs K framework)
112+
```sh
113+
# First, enter the integration nix shell:
114+
nix develop \
115+
github:runtimeverification/k/v$(cat deps/k_release)#kore-integration-tests \
116+
--override-input haskell-backend . --update-input haskell-backend
117+
118+
# Then:
119+
make test-k # all integration tests
120+
make test-k-simplifierx # simplifier-specific subset
121+
make -C test/issue-3344 test # single test
122+
```
123+
124+
---
125+
126+
## Key Architecture: The Two-Engine Proxy
127+
128+
`kore-rpc-booster` runs **two symbolic execution engines in the same process**:
129+
130+
| Engine | Code | LLVM loaded? | Speed |
131+
|--------|------|-------------|-------|
132+
| **Booster** | `booster/library/Booster/` | Yes | Fast |
133+
| **Kore** | `kore/src/Kore/` | No | Slow but complete |
134+
135+
The proxy (`booster/tools/booster/Proxy.hs`) routes each RPC call:
136+
137+
- **`execute`**: Booster runs first. Falls back to Kore (1 step at a time) only when
138+
Booster returns a reason in `fallbackReasons` (default: `Aborted | Stuck | Branching`).
139+
Configurable via `--fallback-on`.
140+
- **`simplify`**: Booster runs, then Kore **always** runs on Booster's output
141+
(see `handleSimplify`, lines 171–214). This is unconditional — even when Booster
142+
has fully simplified the term, Kore is still invoked.
143+
- **`implies`**: Booster first if `assumeDefined=true`, else delegates to Kore.
144+
- **`get-model`**: Booster first; re-checks with Kore only when result is `Unknown`.
145+
- **`add-module`**: Both engines, always.
146+
147+
The `ProxyConfig` record (lines 66–74) controls proxy behaviour:
148+
```haskell
149+
data ProxyConfig = ProxyConfig
150+
{ forceFallback :: Maybe Depth -- force Kore simplification every N steps
151+
, fallbackReasons :: [HaltReason] -- which halt reasons trigger fallback
152+
, simplifyAtEnd :: Bool -- simplify after each execute result
153+
, simplifyBeforeFallback :: Bool -- simplify booster state before kore fallback
154+
, ...
155+
}
156+
```
157+
CLI flags for these fields are defined in `booster/tools/booster/Server.hs` in
158+
`clProxyOptionsParser`.
159+
160+
---
161+
162+
## Booster Internals Quick Reference
163+
164+
**Rewriting** (`Booster/Pattern/Rewrite.hs`):
165+
- Rules are indexed by the head symbol of the `<k>` cell.
166+
- Matching failures are fast; `MatchIndeterminate` (unevaluated functions blocking
167+
unification) causes an abort and triggers a full-pattern simplification pass.
168+
- Priority groups: a group is "complete" when its remainder predicate is UNSAT →
169+
lower-priority rules are skipped.
170+
171+
**Simplification** (`Booster/Pattern/Util.hs`, equation application code):
172+
- Traverses bottom-up, applies function/simplification equations.
173+
- Concrete sub-terms are sent to the LLVM backend for evaluation (top-down first
174+
to maximise batch size).
175+
176+
**Term representation** (`Booster/Pattern/Base.hs`):
177+
- `Term` is a tagged union with a `TermAttributes` field tracking `isConstructorLike`,
178+
`isDefined`, `isSimplified`, etc.
179+
- `isSimplified` signals whether any equation could still apply.
180+
181+
---
182+
183+
## Performance Testing and Analysis
184+
185+
```sh
186+
# Run KEVM performance suite with bug reports
187+
PYTEST_PARALLEL=8 scripts/performance-tests-kevm.sh --bug-report
188+
189+
# Analyse fallback/abort reasons across bug reports
190+
scripts/booster-analysis.sh scripts/bug-reports/kevm-v1.0.417-main
191+
192+
# Run a specific RPC regression test
193+
cd booster/test/rpc-integration && ./runDirectoryTest.sh test-issue-123
194+
```
195+
196+
See `docs/2026-05-25-submitting-test-cases.md` for the full tarball workflow (generating reports,
197+
replaying quickly, converting to tests, rebuilding the LLVM library).
198+
199+
---
200+
201+
## Development Tips
202+
203+
- `../evm-semantics/docs/kore-rpc-booster-logging.md` documents all log levels,
204+
their overhead, and empirical findings from the current Kore-fallback investigation.
205+
- Use `booster-dev` (no Kore fallback) during development to isolate Booster behaviour.
206+
- Log levels: `-l Aborts` for proxy events, `-l Timing` for per-request timing,
207+
`-l SimplifyKore -l Timing` for kore equation attempts (pair with Timing to enable
208+
`contextLoggingEnabled`).
209+
- The `pretty` dev-tool pretty-prints KORE JSON without needing the original K definition:
210+
`cabal run pretty -- ../definition.kore <(jq '.result.state' response.json)`

‎booster/library/Booster/CLOptions.hs‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -238,6 +238,10 @@ allowedLogLevels =
238238
)
239239
, ("TimeProfile", "Logs for timing analysis")
240240
, ("Timing", "Formerly --print-stats")
241+
,
242+
( "KoreCalls"
243+
, "Log structured input/output for every Kore backend invocation (simplify and execute-fallback)"
244+
)
241245
]
242246

243247
levelToContext :: Map Text [ContextFilter]
@@ -282,6 +286,7 @@ levelToContext =
282286
, [ctxt| request*,booster>rewrite*,match|definedness|constraint,abort. |]
283287
, [ctxt| request*,proxy. |]
284288
, [ctxt| request*,proxy,abort. |]
289+
, [ctxt| request*,proxy>abort,detail. |]
285290
, [ctxt| request*,booster>failure,abort |]
286291
]
287292
)
@@ -306,6 +311,18 @@ levelToContext =
306311
[ [ctxt| *>timing |]
307312
]
308313
)
314+
,
315+
( "KoreCalls"
316+
,
317+
[ [ctxt| request*,proxy>detail. |]
318+
]
319+
)
320+
,
321+
( "SimplifyKore"
322+
,
323+
[ [ctxt| request*>simplification*|function*,success |]
324+
]
325+
)
309326
]
310327

311328
-- Partition provided log levels into standard and custom ones, and

‎booster/test/rpc-integration/README.md‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,12 @@ NOTE: You may need to specify `--host 127.0.0.1` on Arch Linux.
4242

4343
Step 2 above can be run using `--expect response-NAME.json --regenerate` to (over-)write the output file.
4444

45+
## How to import a bug-report tarball as a test
46+
47+
See `docs/2026-05-25-submitting-test-cases.md` for the full workflow: generating bug-report tarballs,
48+
replaying them quickly, converting them into a `test-*` directory here, and rebuilding
49+
the LLVM `.dylib` when the definition changes.
50+
4551
## How to pretty-print Kore
4652

4753
Use `tools/rpc-kast.sh` to pretty-print the kore terms from JSON requests and responses into pretty K. Specify the compiled K definition as `K_DEFINITION`. For example:

‎booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -59,6 +59,7 @@
5959
{"context":[{"request":"4"},"booster","simplify",{"term":"ee3511f"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
6060
{"context":[{"request":"4"},"kore","execute",{"term":"8aaaa91"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"c107051"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"...resources/log-simplify-json.kore:3913:7"}
6161
{"context":[{"request":"4"},"kore","execute",{"term":"8aaaa91"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"c107051"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"b378f16"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}}
62+
{"context":[{"request":"4"},"kore","execute",{"term":"8aaaa91"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"c107051"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"a7635c2"},"kore-term"],"message":{"location":"...resources/log-simplify-json.kore:3913:7","result":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}}}
6263
{"context":[{"request":"4"},"booster","simplify",{"term":"ee3511f"},{"term":"dfe34e0"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"}
6364
{"context":[{"request":"4"},"booster","simplify",{"term":"ee3511f"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
6465
{"context":[{"request":"4"},"booster","simplify",{"term":"66aa67b"},{"term":"8f1e2b8"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"}

0 commit comments

Comments
 (0)