search

runtimeverification / evm-semantics

K Semantics of the Ethereum Virtual Machine (EVM)
BSD 3-Clause "New" or "Revised" License
509 stars 144 forks source link

Outdated examples in KEVM #2338

Closed anvacaru closed 8 months ago

anvacaru commented 8 months ago

Most of the Solidity examples in test/specs/examples require the solc-to-k command that was extracted in kontrol. We should either remove them or bring back some of the solc-to-k functionality.

Originally posted by @anvacaru in https://github.com/runtimeverification/evm-semantics/issues/2337#issuecomment-1983382860

ehildenb commented 8 months ago

The Solidity files are nice references for folks looking at those specifications, which have been committed. So I don't really see a need to remove them, but we could add a README explaining that.

I also don't want to pull solc_to_k back to this repo, as it's Solidity specific and we're trying to move Solidity specific things to Kontrol.

ehildenb commented 8 months ago

I don't think this is a bug as much as a documentation issue. And VERIFICATION.md may not be a needed file anymore, using KEVM directly for verification is pretty low-level, we should be pushing people towards Kontrol.