[RaoulSchaffranek]

Warning

Do not merge. This is an experiment to measure a performance idea. It is not ready for review.

The problem

Every request that reaches Kore in the RPC server first prepares all function equations of the definition (Equation.simplifyExtractedEquations, called from evalSimplifier). That is about 3,600 equations for KEVM. It costs 1–3 seconds per request, even for a trivial one. The equations never change once a module is loaded, so this work is repeated for nothing.

This happens on every simplify, implies, execute and get-model that Kore handles, including the fallbacks from Booster.

The change

• makeSerializedModule prepares the equations once, when the module is loaded (or added with add-module), and keeps them in SerializedModule (new field preparedEquations).
• exec, rpcExec, search and the RPC handlers use the stored equations (new evalSimplifierPrepared) instead of preparing them again.
• Everything else stays per request, including the memo of function results.
• evalSimplifier behaves as before for its other callers.

The preparation only reads the module (sort graph, overload graph, metadata tools, extracted equations). It runs in the same environment as before (no equations, no memo, no hooked symbols); only the moment changes.

First measurement

A trivial simplify (the integer 1) on the KEVM definition, five requests on each server, same machine:

	per request	server start-up
kore-rpc-booster 0.1.155	1.45–1.81 s	10.0 s
with this change	0.17–0.21 s	10.8 s

These numbers come from the same change applied to v0.1.155 (branch raoul/reuse-simplifier-0.1.155). This PR is the same commit on master.

Still to check

• The test suites, and that KEVM, Kontrol and KMIR proofs give identical results (we are running these in our benchmark harness).
• Memory: every added module now also keeps its prepared equations.
• The preparation now runs with the SMT solver of the module load, not of the request. The solver has no request-specific assertions at that point, so this should not matter.

🤖 Generated with Claude Code

[Copilot]

🔵 Needs a closer look

Cross-request equation caching and serialized persistence still need maintainer validation of proof-result equivalence and retained-memory behavior under repeated module additions with representative KEVM/Kontrol/KMIR workloads.

No open issues 🎉

What changed in this PR

This experimental PR reduces repeated work in the Kore backend by preparing function equations once per loaded module and reusing them across requests, including Booster fallbacks. It remains marked do not merge, pending correctness and memory validation.

Changes:

• Store prepared equations in SerializedModule during module initialization.
• Reuse them in execution, search, and RPC simplification paths.
• Keep memoization per request and retain on-demand preparation for existing simplifier callers.

File	Description
kore/​src/​Kore/​Simplify/​API.hs	Separates equation preparation from simplifier setup and adds prepared-equation entry points.
kore/​src/​Kore/​JsonRpc.hs	Uses stored prepared equations in RPC handlers.
kore/​src/​Kore/​Exec.hs	Stores prepared equations and reuses them for execution and search.

_{Review effort: Balanced}