Commit Graph

12 Commits

Author SHA1 Message Date
Harikrishnan Mulackal
2b9f040c48 Optimize exp when base is -1 2020-09-29 17:44:09 +02:00
Harikrishnan Mulackal
64ddf2c699 Verify simplification rule exp(2, X) to shl(X, 1) 2020-09-16 17:36:39 +02:00
chriseth
a3a9630d8b Optimize byte-after-shr for shift amounts that are not multiples of 8. 2020-08-04 12:16:23 +02:00
chriseth
59f4989966 Optimize combination of byte and shl. 2020-07-08 20:26:46 +02:00
yoni206
4327434d07 Adding bit-vector NOT operation to the opcodes. 2020-04-28 09:43:31 -07:00
Leonardo Alt
606153ba71 Add optimizer rules for repeated and 2020-04-22 10:20:59 +02:00
Daniel Kirchner
c71fb76bb2 Proofs for the overflow and underflow conditions in checked arithmetic for Sol->Yul code generation. 2019-06-20 15:58:10 +02:00
Leonardo Alt
51ba7f5f17 Add CI job for optimization proofs 2019-06-19 22:29:23 +02:00
chriseth
633510eb04
Merge pull request #6935 from ethereum/subMaxValueXNotXRule
Add optimization rule SUB(~0, X) -> NOT(X).
2019-06-17 14:42:49 +02:00
Daniel Kirchner
5718072e10 Fix comparison opcodes and minor errors in proof scripts. 2019-06-14 17:04:50 +02:00
Daniel Kirchner
d3293cf0d0 Correctness proof for SUB(NOT(0),X)->NOT(X). 2019-06-14 14:08:21 +02:00
Leonardo Alt
5089d4ac28 Move optimization proofs repo to Solidity repo 2019-06-13 17:11:48 +02:00