solidity

cerc-io/solidity

Fork 0

mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00

Files

T

History

chriseth 63c74f5da2 Add non-revert condition.

2022-03-03 14:05:15 +01:00

byte_big.py

test/formal: Get rid of wildcard imports

2021-10-13 16:20:10 +02:00

byte_equivalence.py

test/formal: Get rid of wildcard imports

2021-10-13 16:20:10 +02:00

checked_int_add.py

test/formal: Get rid of wildcard imports

2021-10-13 16:20:10 +02:00

checked_int_div.py

test/formal: Get rid of wildcard imports

2021-10-13 16:20:10 +02:00

checked_int_mul_16.py

test/formal: Get rid of wildcard imports

2021-10-13 16:20:10 +02:00

checked_int_sub.py

test/formal: Get rid of wildcard imports

2021-10-13 16:20:10 +02:00

checked_uint_add.py

test/formal: Get rid of wildcard imports

2021-10-13 16:20:10 +02:00

checked_uint_mul_16.py

test/formal: Get rid of wildcard imports

2021-10-13 16:20:10 +02:00

checked_uint_sub.py

test/formal: Get rid of wildcard imports

2021-10-13 16:20:10 +02:00

combine_byte_shl.py

test/formal: Get rid of wildcard imports

2021-10-13 16:20:10 +02:00

combine_byte_shr_1.py

test/formal: Get rid of wildcard imports

2021-10-13 16:20:10 +02:00

combine_byte_shr_2.py

test/formal: Get rid of wildcard imports

2021-10-13 16:20:10 +02:00

combine_div_shl_one_32.py

test/formal: Get rid of wildcard imports

2021-10-13 16:20:10 +02:00

combine_mul_shl_one_64.py

test/formal: Get rid of wildcard imports

2021-10-13 16:20:10 +02:00

combine_shl_shr_by_constant_64.py

test/formal: Get rid of wildcard imports

2021-10-13 16:20:10 +02:00

combine_shr_shl_by_constant_64.py

test/formal: Get rid of wildcard imports

2021-10-13 16:20:10 +02:00

eq_sub.py

test/formal: Get rid of wildcard imports

2021-10-13 16:20:10 +02:00

exp_neg_one.py

test/formal: Get rid of wildcard imports

2021-10-13 16:20:10 +02:00

exp_to_shl.py

test/formal: Get rid of wildcard imports

2021-10-13 16:20:10 +02:00

move_and_across_shl_128.py

test/formal: Get rid of wildcard imports

2021-10-13 16:20:10 +02:00

move_and_across_shr_128.py

test/formal: Get rid of wildcard imports

2021-10-13 16:20:10 +02:00

move_and_inside_or.py

test/formal: Get rid of wildcard imports

2021-10-13 16:20:10 +02:00

opcodes.py

test/formal: Get rid of wildcard imports

2021-10-13 16:20:10 +02:00

README.md

Move optimization proofs repo to Solidity repo

2019-06-13 17:11:48 +02:00

redundant_store_unrelated.py

Add non-revert condition.

2022-03-03 14:05:15 +01:00

repeated_and.py

test/formal: Get rid of wildcard imports

2021-10-13 16:20:10 +02:00

repeated_or.py

test/formal: Get rid of wildcard imports

2021-10-13 16:20:10 +02:00

replace_mul_by_shift.py

test/formal: Get rid of wildcard imports

2021-10-13 16:20:10 +02:00

rule.py

pylint: Enable and fix no-self-use warnings

2021-12-21 15:30:11 +01:00

shl_workaround_8.py

test/formal: Get rid of wildcard imports

2021-10-13 16:20:10 +02:00

signextend_and.py

test/formal: Get rid of wildcard imports

2021-10-13 16:20:10 +02:00

signextend_equivalence.py

test/formal: Get rid of wildcard imports

2021-10-13 16:20:10 +02:00

signextend_shl.py

test/formal: Get rid of wildcard imports

2021-10-13 16:20:10 +02:00

signextend_shr.py

test/formal: Get rid of wildcard imports

2021-10-13 16:20:10 +02:00

signextend.py

test/formal: Get rid of wildcard imports

2021-10-13 16:20:10 +02:00

sub_not_zero_x_to_not_x_256.py

test/formal: Get rid of wildcard imports

2021-10-13 16:20:10 +02:00

sub_sub.py

test/formal: Get rid of wildcard imports

2021-10-13 16:20:10 +02:00

util.py

test/formal: Get rid of wildcard imports

2021-10-13 16:20: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:

HOL with EthIsabelle
FOL with SMT solvers using Integers and BitVectors