| Name | Date | Size | #Lines | LOC | ||
|---|---|---|---|---|---|---|
| .. | 03-May-2022 | - | ||||
| README.md | H A D | 20-Dec-2021 | 388 | 7 | 4 | |
| byte_big.py | H A D | 20-Dec-2021 | 266 | 20 | 13 | |
| byte_equivalence.py | H A D | 20-Dec-2021 | 580 | 23 | 16 | |
| checked_int_add.py | H A D | 20-Dec-2021 | 1.1 KiB | 41 | 24 | |
| checked_int_div.py | H A D | 20-Dec-2021 | 795 | 37 | 20 | |
| checked_int_mul_16.py | H A D | 20-Dec-2021 | 1.4 KiB | 44 | 26 | |
| checked_int_sub.py | H A D | 20-Dec-2021 | 1.1 KiB | 41 | 24 | |
| checked_uint_add.py | H A D | 20-Dec-2021 | 791 | 37 | 20 | |
| checked_uint_mul_16.py | H A D | 20-Dec-2021 | 873 | 38 | 20 | |
| checked_uint_sub.py | H A D | 20-Dec-2021 | 776 | 37 | 20 | |
| combine_byte_shl.py | H A D | 20-Dec-2021 | 482 | 31 | 20 | |
| combine_byte_shr_1.py | H A D | 20-Dec-2021 | 559 | 32 | 21 | |
| combine_byte_shr_2.py | H A D | 20-Dec-2021 | 384 | 29 | 18 | |
| combine_div_shl_one_32.py | H A D | 20-Dec-2021 | 340 | 26 | 15 | |
| combine_mul_shl_one_64.py | H A D | 20-Dec-2021 | 465 | 32 | 19 | |
| combine_shl_shr_by_constant_64.py | H A D | 20-Dec-2021 | 810 | 46 | 31 | |
| combine_shr_shl_by_constant_64.py | H A D | 20-Dec-2021 | 810 | 46 | 31 | |
| eq_sub.py | H A D | 20-Dec-2021 | 327 | 25 | 14 | |
| exp_neg_one.py | H A D | 20-Dec-2021 | 412 | 18 | 12 | |
| exp_to_shl.py | H A D | 20-Dec-2021 | 727 | 35 | 18 | |
| move_and_across_shl_128.py | H A D | 20-Dec-2021 | 630 | 38 | 23 | |
| move_and_across_shr_128.py | H A D | 20-Dec-2021 | 630 | 38 | 23 | |
| move_and_inside_or.py | H A D | 20-Dec-2021 | 682 | 35 | 20 | |
| opcodes.py | H A D | 20-Dec-2021 | 1.4 KiB | 82 | 60 | |
| repeated_and.py | H A D | 20-Dec-2021 | 698 | 41 | 26 | |
| repeated_or.py | H A D | 20-Dec-2021 | 675 | 41 | 26 | |
| replace_mul_by_shift.py | H A D | 20-Dec-2021 | 598 | 39 | 26 | |
| rule.py | H A D | 20-Dec-2021 | 974 | 45 | 34 | |
| shl_workaround_8.py | H A D | 20-Dec-2021 | 535 | 29 | 20 | |
| signextend.py | H A D | 20-Dec-2021 | 737 | 38 | 27 | |
| signextend_and.py | H A D | 20-Dec-2021 | 538 | 28 | 21 | |
| signextend_equivalence.py | H A D | 20-Dec-2021 | 567 | 26 | 19 | |
| signextend_shl.py | H A D | 20-Dec-2021 | 550 | 27 | 21 | |
| signextend_shr.py | H A D | 20-Dec-2021 | 595 | 32 | 26 | |
| sub_not_zero_x_to_not_x_256.py | H A D | 20-Dec-2021 | 347 | 28 | 15 | |
| sub_sub.py | H A D | 20-Dec-2021 | 606 | 38 | 31 | |
| util.py | H A D | 20-Dec-2021 | 738 | 28 | 22 |
README.md
1The Solidity compiler implements several [optimization rules](https://github.com/ethereum/solidity/blob/develop/libevmasm/RuleList.h). 2 3This directory contains an effort to formally prove the correctness of those rules in: 4 5- HOL with [EthIsabelle](https://github.com/ekpyron/eth-isabelle) 6- FOL with SMT solvers using [Integers and BitVectors](http://smtlib.cs.uiowa.edu/theories.shtml) 7