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
Files
avoidNeedlessPopping
solidity/test/formal
T
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
Proofs for the overflow and underflow conditions in checked arithmetic for Sol->Yul code generation.
2019-06-20 15:58:10 +02:00
checked_int_div.py
Proofs for the overflow and underflow conditions in checked arithmetic for Sol->Yul code generation.
2019-06-20 15:58:10 +02:00
checked_int_mul_16.py
Proofs for the overflow and underflow conditions in checked arithmetic for Sol->Yul code generation.
2019-06-20 15:58:10 +02:00
checked_int_sub.py
Proofs for the overflow and underflow conditions in checked arithmetic for Sol->Yul code generation.
2019-06-20 15:58:10 +02:00
checked_uint_add.py
Proofs for the overflow and underflow conditions in checked arithmetic for Sol->Yul code generation.
2019-06-20 15:58:10 +02:00
checked_uint_mul_16.py
Proofs for the overflow and underflow conditions in checked arithmetic for Sol->Yul code generation.
2019-06-20 15:58:10 +02:00
checked_uint_sub.py
Proofs for the overflow and underflow conditions in checked arithmetic for Sol->Yul code generation.
2019-06-20 15:58:10 +02:00
combine_byte_shl.py
Optimize combination of byte and shl.
2020-07-08 20:26:46 +02:00
combine_byte_shr_1.py
Optimize combination of byte and shl.
2020-07-08 20:26:46 +02:00
combine_byte_shr_2.py
Optimize byte-after-shr for shift amounts that are not multiples of 8.
2020-08-04 12:16:23 +02:00
combine_div_shl_one_32.py
Fix comparison opcodes and minor errors in proof scripts.
2019-06-14 17:04:50 +02:00
combine_mul_shl_one_64.py
Fix comparison opcodes and minor errors in proof scripts.
2019-06-14 17:04:50 +02:00
combine_shl_shr_by_constant_64.py
Move optimization proofs repo to Solidity repo
2019-06-13 17:11:48 +02:00
combine_shr_shl_by_constant_64.py
Fix comparison opcodes and minor errors in proof scripts.
2019-06-14 17:04:50 +02:00
eq_sub.py
Optimize iszero(sub(x, y)) to eq(x, y).
2020-12-22 15:11:48 +01:00
exp_neg_one.py
Optimize exp when base is -1
2020-09-29 17:44:09 +02:00
exp_to_shl.py
Verify simplification rule exp(2, X) to shl(X, 1)
2020-09-16 17:36:39 +02:00
move_and_across_shl_128.py
Move optimization proofs repo to Solidity repo
2019-06-13 17:11:48 +02:00
move_and_across_shr_128.py
Move optimization proofs repo to Solidity repo
2019-06-13 17:11:48 +02:00
move_and_inside_or.py
Move AND with constant inside OR.
2021-03-09 15:26:19 +01:00
opcodes.py
Formalization of SIGNEXTEND and rule proofs
2021-08-16 18:54:33 +02:00
README.md
Move optimization proofs repo to Solidity repo
2019-06-13 17:11:48 +02:00
repeated_and.py
Add optimizer rules for repeated and
2020-04-22 10:20:59 +02:00
repeated_or.py
Add optimizer rules for repeated and
2020-04-22 10:20:59 +02:00
replace_mul_by_shift.py
Proof.
2021-03-18 08:42:49 +01:00
rule.py
Add CI job for optimization proofs
2019-06-19 22:29:23 +02:00
shl_workaround_8.py
Move optimization proofs repo to Solidity repo
2019-06-13 17:11:48 +02:00
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
Correctness proof for SUB(NOT(0),X)->NOT(X).
2019-06-14 14:08:21 +02:00
sub_sub.py
Proof for rules.
2021-08-19 12:51:54 +02:00
util.py
Proofs for the overflow and underflow conditions in checked arithmetic for Sol->Yul code generation.
2019-06-20 15:58:10 +02:00

README.md

The Solidity compiler implements several optimization rules.

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

Reference in New Issue View Git Blame Copy Permalink