search

pirapira / eth-isabelle

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

Pirapira master #438

Closed seed closed 7 years ago

seed commented 7 years ago

Huge cleanup. Use sep-algebra instead of ad-hoc separation logic framework. Pack pretty much all rules added to simpset in bundles. Fix existing proofs.

pirapira commented 7 years ago

Thanks a lot!