Repository navigation
[WIP] Try a K frontend that loads claims faster (k#4943) - #2883
Draft
RaoulSchaffranek wants to merge 1 commit into
Draft
RaoulSchaffranek wants to merge 1 commit into
RaoulSchaffranek wants to merge 1 commit into
Conversation
…nch raoul/kprove-spec-steps) The K branch makes kprove apply the specification steps only to the spec's own modules, which shortens `kprove --dry-run --emit-json-spec` (claim loading in `kevm prove`). - flake.nix, flake.lock: k-framework at that K commit. - deps/k_frontend_rev: the K commit whose k-frontend jar the CI Docker image uses. The image is still based on the K release in deps/k_release; only the k-frontend jar is rebuilt from the commit and swapped in. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This branch has not been deployed
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
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.
What is slow
Before
kevm provecan prove anything in a spec file, it loads the claims withkprove --dry-run --emit-json-spec. This takes 18–37 s per spec file (median 24 s), about 4,000 s over the 159 spec files of the proof suites. Most of it is spent in K's specification steps. They are applied to the spec module and to the whole KEVM semantics it imports, and the result for the semantics is then discarded.What this changes
runtimeverification/k#4943 applies those steps only to the spec's own modules. This PR uses that K:
flake.nix,flake.lock:k-frameworkpoints at the K commit instead ofv7.1.337.deps/k_frontend_rev(new): the same K commit. The CI Docker image is still built from the K release indeps/k_release. The Dockerfile now builds thek-frontendjar from this commit and puts it in place of the release's jar. The K change is only in the Java frontend, and the commit is based on v7.1.337, so the rest of the release stays valid.The Python side does not change (
kframework==7.1.337).What was checked
All on one machine, outside CI:
kproveemits the same claims as the unpatched one: byte-identical for 138, the same claims in a different order for 21 (unpatchedkprovealready varies in claim order between runs).kprove --dry-run --emit-json-spec, sequential runs on 8 cores at a load average of 3–5: about 35–48 s before and 12–18 s after, on benchmarks/address00, erc20/ds/approve-success, mcd/dai-adduu-fail-rough, functional/lemmas and benchmarks/functional. Details are in [WIP] kprove: apply the specification steps only to the spec's own modules k#4943.Still open
k-frontendjar has not been run yet. This PR's CI is its first test.deps/k_releaseas usual.🤖 Generated with Claude Code