From d46da8e53c880cf44ff7d4c431c41bf1844debb3 Mon Sep 17 00:00:00 2001
From: chriseth <chris@ethereum.org>
Date: Tue, 22 Dec 2020 15:08:37 +0100
Subject: [PATCH 1/2] Optimize iszero(sub(x, y)) to eq(x, y).

---
 libevmasm/RuleList.h                          |  5 ++++
 test/formal/eq_sub.py                         | 23 +++++++++++++++++++
 .../expressionSimplifier/sub_eq.yul           | 16 +++++++++++++
 3 files changed, 44 insertions(+)
 create mode 100644 test/formal/eq_sub.py
 create mode 100644 test/libyul/yulOptimizerTests/expressionSimplifier/sub_eq.yul

diff --git a/libevmasm/RuleList.h b/libevmasm/RuleList.h
index 8943c662b..c324514ec 100644
--- a/libevmasm/RuleList.h
+++ b/libevmasm/RuleList.h
@@ -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;
 }
 
diff --git a/test/formal/eq_sub.py b/test/formal/eq_sub.py
new file mode 100644
index 000000000..bf7518acf
--- /dev/null
+++ b/test/formal/eq_sub.py
@@ -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)
diff --git a/test/libyul/yulOptimizerTests/expressionSimplifier/sub_eq.yul b/test/libyul/yulOptimizerTests/expressionSimplifier/sub_eq.yul
new file mode 100644
index 000000000..5380c1905
--- /dev/null
+++ b/test/libyul/yulOptimizerTests/expressionSimplifier/sub_eq.yul
@@ -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) }
+// }

From 308549f950be372cc62f3ac2c8243bd71183d32d Mon Sep 17 00:00:00 2001
From: Daniel Kirchner <daniel@ekpyron.org>
Date: Wed, 6 Jan 2021 11:30:28 +0100
Subject: [PATCH 2/2] Simplify test and add Changelog entry.

---
 Changelog.md                                                  | 1 +
 .../expressionSimplifier/{sub_eq.yul => iszero_sub_to_eq.yul} | 4 ++--
 2 files changed, 3 insertions(+), 2 deletions(-)
 rename test/libyul/yulOptimizerTests/expressionSimplifier/{sub_eq.yul => iszero_sub_to_eq.yul} (73%)

diff --git a/Changelog.md b/Changelog.md
index 6c3e1ba4f..e81de927c 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -4,6 +4,7 @@ Language Features:
  * Possibility to use ``catch Panic(uint code)`` to catch a panic failure from an external call.
 
 Compiler Features:
+ * Optimizer: Add rule to replace ``iszero(sub(x,y))`` by ``eq(x,y)``.
  * Parser: Report meaningful error if parsing a version pragma failed.
  * SMTChecker: Support ABI functions as uninterpreted functions.
 
diff --git a/test/libyul/yulOptimizerTests/expressionSimplifier/sub_eq.yul b/test/libyul/yulOptimizerTests/expressionSimplifier/iszero_sub_to_eq.yul
similarity index 73%
rename from test/libyul/yulOptimizerTests/expressionSimplifier/sub_eq.yul
rename to test/libyul/yulOptimizerTests/expressionSimplifier/iszero_sub_to_eq.yul
index 5380c1905..7efa54b02 100644
--- a/test/libyul/yulOptimizerTests/expressionSimplifier/sub_eq.yul
+++ b/test/libyul/yulOptimizerTests/expressionSimplifier/iszero_sub_to_eq.yul
@@ -2,7 +2,7 @@
     let a := calldataload(0)
     let b := calldataload(0x20)
     let x := sub(a, b)
-    if gt(x, 0) {
+    if iszero(x) {
         sstore(0, 1)
     }
 }
@@ -12,5 +12,5 @@
 // {
 //     let _1 := 0
 //     let a := calldataload(_1)
-//     if iszero(eq(a, calldataload(0x20))) { sstore(_1, 1) }
+//     if eq(a, calldataload(0x20)) { sstore(_1, 1) }
 // }