search

pirapira / eth-isabelle

A Lem formalization of EVM and some Isabelle/HOL proofs
Other
237 stars 42 forks source link

Fixed HoareTripleForMemory.thy, MLOAD, MSTORE, but not SHA3 #443

Closed mrsmkl closed 7 years ago

mrsmkl commented 7 years ago

The proof for MSTORE is not yet optimized or cleaned up.

pirapira commented 7 years ago

Thank you!