From c6473ff32b2acf33a5b3cf0fe7c06ca3bf568735 Mon Sep 17 00:00:00 2001
From: chriseth <chris@ethereum.org>
Date: Wed, 18 Aug 2021 23:10:32 +0200
Subject: [PATCH] Proof for rules.

---
 test/formal/sub_sub.py | 36 ++++++++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)
 create mode 100644 test/formal/sub_sub.py

diff --git a/test/formal/sub_sub.py b/test/formal/sub_sub.py
new file mode 100644
index 000000000..d6099c91f
--- /dev/null
+++ b/test/formal/sub_sub.py
@@ -0,0 +1,36 @@
+from rule import Rule
+from opcodes import *
+
+"""
+Rules:
+SUB(SUB(X, A), Y) -> SUB(SUB(X, Y), A)
+SUB(SUB(A, X), Y) -> SUB(A, ADD(X, Y))
+SUB(X, SUB(Y, A)) -> ADD(SUB(X, Y), A)
+SUB(X, SUB(A, Y)) -> ADD(ADD(X, Y), -A)
+"""
+
+rule = Rule()
+
+n_bits = 256
+
+# Input vars
+X = BitVec('X', n_bits)
+Y = BitVec('Y', n_bits)
+A = BitVec('A', n_bits)
+
+rule.check(
+    SUB(SUB(X, A), Y),
+    SUB(SUB(X, Y), A)
+)
+rule.check(
+    SUB(SUB(A, X), Y),
+    SUB(A, ADD(X, Y))
+)
+rule.check(
+    SUB(X, SUB(Y, A)),
+    ADD(SUB(X, Y), A)
+)
+rule.check(
+    SUB(X, SUB(A, Y)),
+    ADD(ADD(X, Y), SUB(0, A))
+)