Optimize iszero(sub(x, y)) to eq(x, y).

This commit is contained in:
chriseth 2020-12-22 15:08:37 +01:00
parent 6bcae84610
commit d46da8e53c
3 changed files with 44 additions and 0 deletions

View File

@ -365,6 +365,11 @@ std::vector<SimplificationRule<Pattern>> simplificationRuleListPart6(
[=]() -> Pattern { return Builtins::EQ(X, Y); }
});
rules.push_back({
Builtins::ISZERO(Builtins::SUB(X, Y)),
[=]() -> Pattern { return Builtins::EQ(X, Y); }
});
return rules;
}

23
test/formal/eq_sub.py Normal file
View File

@ -0,0 +1,23 @@
from rule import Rule
from opcodes import *
"""
Rule:
ISZERO(SUB(X, Y)) -> EQ(X, Y)
"""
rule = Rule()
n_bits = 256
# Input vars
X = BitVec('X', n_bits)
Y = BitVec('Y', n_bits)
# Non optimized result
nonopt = ISZERO(SUB(X, Y))
# Optimized result
opt = EQ(X, Y)
rule.check(nonopt, opt)

View File

@ -0,0 +1,16 @@
{
let a := calldataload(0)
let b := calldataload(0x20)
let x := sub(a, b)
if gt(x, 0) {
sstore(0, 1)
}
}
// ----
// step: expressionSimplifier
//
// {
// let _1 := 0
// let a := calldataload(_1)
// if iszero(eq(a, calldataload(0x20))) { sstore(_1, 1) }
// }