search

formal-land / coq-of-python

Translate Python code to Coq code for formal verification. Applied to the reference implementation of Ethereum in Python.
MIT License
30 stars 0 forks source link

Simulation for the Keccak instruction #15

Closed clarus closed 4 months ago

clarus commented 5 months ago

Write a simulation for the Keccak instruction in https://github.com/ethereum/execution-specs/blob/master/src/ethereum/paris/vm/instructions/keccak.py :