cerc-io/solidity
15
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

Correctness proof for SUB(NOT(0),X)->NOT(X).

Browse Source
This commit is contained in:
Daniel Kirchner 2019-06-14 14:08:21 +02:00
parent 7f322c9433
commit d3293cf0d0
1 changed files with 26 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

26
test/formal/sub_not_zero_x_to_not_x_256.py Normal file
View File

@ -0,0 +1,26 @@
from rule import Rule
from opcodes import *
"""
Rule:
SUB(~0, X) -> NOT(X)
Requirements:
"""
rule = Rule()
n_bits = 256
# Input vars
X = BitVec('X', n_bits)
# Constants
ZERO = BitVecVal(0, n_bits)
# Non optimized result
nonopt = SUB(~ZERO, X)
# Optimized result
opt = NOT(X)
rule.check(nonopt, opt)