runtimeverification / kontrol

BSD 3-Clause "New" or "Revised" License
46 stars 5 forks source link

Move Solidity-specific files to Kontrol repo #180

Open ehildenb opened 9 months ago

ehildenb commented 9 months ago

Several files in KEVM are really solidity specific, which means they belong in Kontrol, for example:

I suspect that these files aren't really needed in KEVM anymore, and so can be moved to Kontrol, and this would avoid issues where those files are updated, a bug is introduced, and not discovered until the merge into Kontrol (for example https://github.com/runtimeverification/evm-semantics/pull/2174).

tothtamas28 commented 9 months ago

hashed-locations.md is required by some tests in evm-semantics: https://github.com/runtimeverification/evm-semantics/actions/runs/6892722711/job/18750760600?pr=2180

anvacaru commented 9 months ago

Both abi.md and hashed-locations.md are required in the edsl.md module which handles the syntactic sugar for kevm claims. It might be easier to move the entire module to Kontrol.