runtimeverification / runtimeverification/evm-semantics

Add dedicated SourceTarget to kdist

Open
#2,777 0 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

Dominant language
KCL
Stars
591
Forks
156
Avg merge
2h 19m
Merged PRs (30d)
1

Description

Currently, evm-semantics is built by building the KEVMTarget kdist target. This target depends on the plugin and also builds KEVM with the given plugin using the function kevm_kompile. Other projects that derive from KEVM such as kontrol and kontrol-node also build KEVM with additional k source files and another main k file and module. While these source files can be successfully added to kompile args, these source files are not tracked by the manifest that uses the Target method source. Additionally, a requirement by pyk is that all referenced source files in the method source must be available in the python module. That means that one cannot inherit from KEVM to override source and keep all referenced files in tact. At the same time, a source target dependency cannot be injected into KEVMTarget, because dependencies are returned by the Target method deps. This is why kontrol and kontrol-node builds always generate the same hash in the kdist cache. In oder to successfully build kontrol or kontrol-node, kdist must be cleaned prior to building. This causes kdist to always unnecessarily rebuild the KEVM plugin, which is slow.

To fix this, the SourceTarget pattern used in web assembly and risc-v semantics repositories can be used. This can be first implemented in evm-semantics and afterwards adapted in kontrol and kontrol-node respectively.

Contributor guide

No contributing guide indexed for this repository

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

Research direction

Start at the KEVMTarget and kevm_kompile entry points, focusing on how Target.source and Target.deps affect manifest tracking. Compare the SourceTarget pattern in the linked skribe src/skribe/kdist/plugin.py, then implement it first for evm-semantics. Done means the additional sources are tracked and derived builds no longer require cleaning kdist to avoid the same cache hash.

Written by the indexing model from the issue text.

Assessment

Tech stack
python
Domain
build-system, tooling
Issue type
Feature
Difficulty
4/5
Estimated time
3-5 days
Activity status
Stale
Clarity
Mostly clear
Newbie friendliness
42/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.