cerc-io/solidity
11
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity
aab6b8a3d7
solidity/test/formal
History
chriseth c6473ff32b Proof for rules.
2021-08-19 12:51:54 +02:00
..
byte_big.py Fix implementation of BYTE 2021-08-09 19:14:14 +02:00
byte_equivalence.py An equivalence check for the Byte opcode 2021-08-10 11:00:29 +02:00
checked_int_add.py
checked_int_div.py
checked_int_mul_16.py
checked_int_sub.py
checked_uint_add.py
checked_uint_mul_16.py
checked_uint_sub.py
combine_byte_shl.py
combine_byte_shr_1.py
combine_byte_shr_2.py
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
eq_sub.py
exp_neg_one.py
exp_to_shl.py
move_and_across_shl_128.py
move_and_across_shr_128.py
move_and_inside_or.py
opcodes.py Formalization of SIGNEXTEND and rule proofs 2021-08-16 18:54:33 +02:00
README.md
repeated_and.py
repeated_or.py
replace_mul_by_shift.py Proof. 2021-03-18 08:42:49 +01:00
rule.py
shl_workaround_8.py
signextend_and.py Formalization of SIGNEXTEND and rule proofs 2021-08-16 18:54:33 +02:00
signextend_equivalence.py An equivalence check for SIGNEXTEND opcode 2021-08-16 18:54:33 +02:00
signextend_shl.py Formalization of SIGNEXTEND and rule proofs 2021-08-16 18:54:33 +02:00
signextend_shr.py Formalization of SIGNEXTEND and rule proofs 2021-08-16 18:54:33 +02:00
signextend.py Formalization of SIGNEXTEND and rule proofs 2021-08-16 18:54:33 +02:00
sub_not_zero_x_to_not_x_256.py
sub_sub.py Proof for rules. 2021-08-19 12:51:54 +02:00
util.py

README.md

The Solidity compiler implements several optimization rules.

This directory contains an effort to formally prove the correctness of those rules in: