EVM - Wasm Interoperability

[bbyalcinkaya]

This PR integrates the Stylus semantics directly into the KEVM semantics, delivering a unified execution and state model for both Stylus (Wasm) and Solidity (EVM) contracts, and enables EVM <-> WASM cross-vm calls. The key changes include:

• Included the EVM semantics into the project and updated the compilation targets to successfully build the project with all necessary dependencies.
• Refactored the Stylus semantics to be built on top of EVM semantics; unified blockchain state management under the <kevm> cell, including all account data.
• Introduced the <stylusvm> cell to manage Stylus contract execution context. The <stylusvm> cell contains the <wasm> cell and the <stylusStack> cell.
• Implemented semantics to support inter-contract calls between EVM and Wasm contracts in both directions.
• Added interoperability tests to validate seamless cross-language contract interactions.

[bbyalcinkaya]

🔧 Installation

Clone the repository (including submodules) and checkout to this branch:

git clone --recurse-submodules https://github.com/runtimeverification/skribe.git
cd skribe
git checkout evm

1. Install the K Framework

bash <(curl https://kframework.org/install)
kup install k

2. Install UV (Python dependency manager)

curl -LsSf https://astral.sh/uv/install.sh | sh

3. Build the Stylus semantics

make kdist-build

▶️ Usage

Working examples are included and exercised in our CI.

• src/tests/integration/data/simulation/call_counter_evm_to_wasm.json
• src/tests/integration/data/simulation/call_counter_wasm_to_evm.json

First, build the contracts involved in the simulation:

make test-contracts

Then, run the simulation test:

uv run skribe-simulation run src/tests/integration/data/simulation/call_counter_evm_to_wasm.json

✅ A 0 exit code denotes success.

[juliankuners]

nix changes LGTM