mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
| .. | ||
| combine_div_shl_one_32.py | ||
| combine_mul_shl_one_64.py | ||
| combine_shl_shr_by_constant_64.py | ||
| combine_shr_shl_by_constant_64.py | ||
| move_and_across_shl_128.py | ||
| move_and_across_shr_128.py | ||
| opcodes.py | ||
| README.md | ||
| rule.py | ||
| shl_workaround_8.py | ||
The Solidity compiler implements several optimization rules.
This directory contains an effort to formally prove the correctness of those rules in:
- HOL with EthIsabelle
- FOL with SMT solvers using Integers and BitVectors