using this semantics in Coq

[aa755]

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]

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]

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