Foundry support

[bbyalcinkaya]

Foundry Integration for Skribe

• Added support for building and running Foundry fuzz tests via Skribe.
• Skribe now automatically detects whether a project is a Foundry (Solidity) project or a Stylus (Rust) project when running skribe build and skribe run. Solidity projects are built using Forge under the hood.
• Integrated Kontrol semantics to support Foundry cheatcodes.
• Implemented concrete semantics for the vm.assume cheatcode to enable fuzzing.
  • In Kontrol, #assume is implemented using the ensures clause, which only has an effect in symbolic execution.
  • In Skribe, concrete semantics are needed for #assume to work during fuzzing:
    • #assume(true) acts as a no-op and execution continues normally.
    • #assume(false) ends execution immediately, treating it as a successful termination (exit code 0), since the path guarded by the assumption is considered infeasible.

Integration tests and verification

Integration tests were added to exercise Foundry cheatcodes in various scenarios. Solidity fuzz tests were used to verify that Skribe can successfully build (skribe build) and run (skribe run) Foundry tests end-to-end, ensuring proper handling of state updates, event emission, and returned values. Example tests include:

• Using vm.prank to simulate calls from different addresses.
• Asserting reverts with vm.expectRevert.
• Checking emitted events via vm.expectEmit.
• Applying vm.assume to filter generated fuzzing inputs.

Decision Tree Optimizations

Applied several targeted semantics optimizations to reduce the decision tree size from ~1GB to ~665MB.

• Simplify autoalloc.md: The autoalloc.md module is responsible for resolving imports in WASM modules and linking them to host functions. Initially, this was a generic module, but it was specialized for Stylus host function imports.

• Empty <stylusvms> in Skribe commands: Some Skribe commands only apply when there is no active Stylus VM (Wasm) running. Since these commands (e.g. callStylus, checkOutput) are executed at the very beginning and end of execution, the <stylusvms> cell can be assumed empty.

• Mention <k> cell in hostcall rules: Host calls are implemented as internal WASM instructions. During their execution, the <k> cell typically contains #endWasm, since the actual execution is being handled in the <instrs> cell. By making this explicit in the rules, the decision tree was reduced from 800 MB → 690 MB.

---

Installation and Usage

Installation

Install the K framework:

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

Install the UV Python dependency manager:

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

Clone the Skribe repository (including submodules) and check out the this branch:

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

Build the semantics:

make kdist

Usage

Navigate to the test contract's directory

cd src/tests/integration/data/contracts/test-foundry-hello/

Build the contract and run the tests:

uv run skribe build
uv run skribe run