Upstreaming Kontrol slot update lemmas as tests

runtimeverification / evm-semantics

K Semantics of the Ethereum Virtual Machine (EVM)

BSD 3-Clause "New" or "Revised" License

509 stars 144 forks source link

Closed PetarMax closed 2 months ago

PetarMax commented 2 months ago

This PR brings in six slot-update-related lemmas from Kontrol as tests, as they are now provable.