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

using this semantics in Coq #2552

Open aa755 opened 3 months ago

aa755 commented 3 months ago

Has anyone explored how to use the KEVM semantics in Coq? Is there a generic K to Coq translator or has someone written a specific translation for KEVM?

I would like to use this semantics to prove correctness of an implementation of an optimized EVM interpretor or jit compliler.

ehildenb commented 3 months ago

One approach would be to use Kamelo: https://gitlab.com/semantiko/kamelo. That was a project by Inria to emit Dedukti from K definitions, and then you can emit Coq from Dedukti.

ehildenb commented 3 months ago

And another thing to study, as more of a deep embedding approach: https://arxiv.org/pdf/2201.05716