Merge pull request #6939 from ethereum/opt_proofs

Move optimization proofs repo to Solidity repo

test/formal/README.md

@@ -0,0 +1,6 @@
+The Solidity compiler implements several [optimization rules](https://github.com/ethereum/solidity/blob/develop/libevmasm/RuleList.h).
+
+This directory contains an effort to formally prove the correctness of those rules in:
+
+- HOL with [EthIsabelle](https://github.com/ekpyron/eth-isabelle)
+- FOL with SMT solvers using [Integers and BitVectors](http://smtlib.cs.uiowa.edu/theories.shtml)

test/formal/combine_div_shl_one_32.py

@@ -0,0 +1,27 @@
+from rule import Rule
+from opcodes import *
+
+"""
+Rule:
+DIV(X, SHL(Y, 1)) -> SHR(Y, X)
+Requirements:
+"""
+
+rule = Rule()
+
+n_bits = 32
+
+# Input vars
+X = BitVec('X', n_bits)
+Y = BitVec('Y', n_bits)
+
+# Constants
+ONE = BitVecVal(1, n_bits)
+
+# Non optimized result
+nonopt = DIV(X, SHL(Y, ONE))
+
+# Optimized result
+opt = SHR(Y, X)
+
+rule.check(nonopt, opt)

test/formal/combine_mul_shl_one_64.py

@@ -0,0 +1,33 @@
+from rule import Rule
+from opcodes import *
+
+"""
+Rule:
+MUL(X, SHL(Y, 1)) -> SHL(Y, X)
+MUL(SHL(X, 1), Y) -> SHL(X, Y)
+Requirements:
+"""
+
+rule = Rule()
+
+n_bits = 64
+
+# Input vars
+X = BitVec('X', n_bits)
+Y = BitVec('Y', n_bits)
+
+# Constants
+ONE = BitVecVal(1, n_bits)
+
+# Requirements
+
+# Non optimized result
+nonopt_1 = MUL(X, SHL(Y, ONE))
+nonopt_2 = MUL(SHL(X, ONE), Y)
+
+# Optimized result
+opt_1 = SHL(Y, X)
+opt_2 = SHL(X, Y)
+
+rule.check(nonopt_1, opt_1)
+rule.check(nonopt_2, opt_2)

test/formal/combine_shl_shr_by_constant_64.py

@@ -0,0 +1,44 @@
+from rule import Rule
+from opcodes import *
+
+"""
+Rule:
+mask = shlWorkaround(u256(-1), unsigned(A.d())) >> unsigned(B.d())
+SHR(B, SHL(A, X)) -> AND(SH[L/R]([B - A / A - B], X), Mask)
+Requirements:
+A < BitWidth
+B < BitWidth
+"""
+
+rule = Rule()
+
+n_bits = 64
+
+# Input vars
+X = BitVec('X', n_bits)
+A = BitVec('A', n_bits)
+B = BitVec('B', n_bits)
+
+# Constants
+BitWidth = BitVecVal(n_bits, n_bits)
+
+# Requirements
+rule.require(ULT(A, BitWidth))
+rule.require(ULT(B, BitWidth))
+
+# Non optimized result
+nonopt = SHR(B, SHL(A, X))
+
+# Optimized result
+Mask = SHR(B, SHL(A, Int2BV(IntVal(-1), n_bits)))
+opt = If(
+	UGT(A, B),
+	AND(SHL(A - B, X), Mask),
+		If(
+			UGT(B, A),
+			AND(SHR(B - A, X), Mask),
+			AND(X, Mask)
+		)
+	)
+
+rule.check(nonopt, opt)

test/formal/combine_shr_shl_by_constant_64.py

@@ -0,0 +1,44 @@
+from rule import Rule
+from opcodes import *
+
+"""
+Rule:
+mask = shlWorkaround(u256(-1) >> unsigned(A.d()), unsigned(B.d()))
+SHL(B, SHR(A, X)) -> AND(SH[L/R]([B - A / A - B], X), Mask)
+Requirements:
+A < BitWidth
+B < BitWidth
+"""
+
+rule = Rule()
+
+n_bits = 64
+
+# Input vars
+X = BitVec('X', n_bits)
+A = BitVec('A', n_bits)
+B = BitVec('B', n_bits)
+
+# Constants
+BitWidth = BitVecVal(n_bits, n_bits)
+
+# Requirements
+rule.require(ULT(A, BitWidth))
+rule.require(ULT(B, BitWidth))
+
+# Non optimized result
+nonopt = SHL(B, SHR(A, X))
+
+# Optimized result
+Mask = SHL(B, SHR(A, Int2BV(IntVal(-1), n_bits)))
+opt = If(
+	UGT(A, B),
+	AND(SHR(a - b, x), Mask),
+		If(
+			UGT(B, A),
+			AND(SHL(B - A, X), Mask),
+			AND(X, Mask)
+		)
+	)
+
+rule.check(nonopt, opt)

test/formal/move_and_across_shl_128.py

@@ -0,0 +1,36 @@
+from rule import Rule
+from opcodes import *
+
+"""
+Rule:
+SHL(B, AND(X, A)) -> AND(SHL(B, X), A << B)
+SHL(B, AND(A, X)) -> AND(SHL(B, X), A << B)
+Requirements:
+B < BitWidth
+"""
+
+rule = Rule()
+
+n_bits = 128
+
+# Input vars
+X = BitVec('X', n_bits)
+A = BitVec('A', n_bits)
+B = BitVec('B', n_bits)
+
+# Constants
+BitWidth = BitVecVal(n_bits, n_bits)
+
+# Requirements
+rule.require(ULT(B, BitWidth))
+
+# Non optimized result
+nonopt_1 = SHL(B, AND(X, A))
+nonopt_2 = SHL(B, AND(A, X))
+
+# Optimized result
+Mask = SHL(B, A)
+opt = AND(SHL(B, X), Mask)
+
+rule.check(nonopt_1, opt)
+rule.check(nonopt_2, opt)

test/formal/move_and_across_shr_128.py

@@ -0,0 +1,36 @@
+from rule import Rule
+from opcodes import *
+
+"""
+Rule:
+SHR(B, AND(X, A)) -> AND(SHR(B, X), A >> B)
+SHR(B, AND(A, X)) -> AND(SHR(B, X), A >> B)
+Requirements:
+B < BitWidth
+"""
+
+rule = Rule()
+
+n_bits = 128
+
+# Input vars
+X = BitVec('X', n_bits)
+A = BitVec('A', n_bits)
+B = BitVec('B', n_bits)
+
+# Constants
+BitWidth = BitVecVal(n_bits, n_bits)
+
+# Requirements
+rule.require(ULT(B, BitWidth))
+
+# Non optimized result
+nonopt_1 = SHR(B, AND(X, A));
+nonopt_2 = SHR(B, AND(A, X));
+
+# Optimized result
+Mask = SHR(B, A);
+opt = AND(SHR(B, X), Mask);
+
+rule.check(nonopt_1, opt)
+rule.check(nonopt_2, opt)

test/formal/opcodes.py

@@ -0,0 +1,46 @@
+from z3 import *
+
+def ADD(x, y):
+	return x + y
+
+def MUL(x, y):
+	return x * y
+
+def SUB(x, y):
+	return x - y
+
+def DIV(x, y):
+	return If(y == 0, 0, UDiv(x, y))
+
+def SDIV(x, y):
+	return If(y == 0, 0, x / y)
+
+def MOD(x, y):
+	return If(y == 0, 0, URem(x, y))
+
+def SMOD(x, y):
+	return If(y == 0, 0, x % y)
+
+def LT(x, y):
+	return ULT(x, y)
+
+def GT(x, y):
+	return UGT(x, y)
+
+def SLT(x, y):
+	return x < y
+
+def SGT(x, y):
+	return x > y
+
+def AND(x, y):
+	return x & y
+
+def SHL(x, y):
+	return y << x
+
+def SHR(x, y):
+	return LShR(y, x)
+
+def SAR(x, y):
+	return y >> x

test/formal/rule.py

@@ -0,0 +1,38 @@
+from z3 import *
+
+class Rule:
+	def __init__(self):
+		self.requirements = []
+		self.constraints = []
+		self.solver = Solver()
+		self.setTimeout(60000)
+
+	def setTimeout(self, _t):
+		self.solver.set("timeout", _t)
+
+	def __lshift__(self, _c):
+		self.constraints.append(_c)
+
+	def require(self, _r):
+		self.requirements.append(_r)
+
+	def check(self, _nonopt, _opt):
+		self.solver.add(self.requirements)
+		result = self.solver.check()
+
+		if result == unknown:
+			raise BaseException('Unable to satisfy requirements.')
+		elif result == unsat:
+			raise BaseException('Requirements are unsatisfiable.')
+
+		self.solver.push()
+		self.solver.add(self.constraints)
+		self.solver.add(_nonopt != _opt)
+
+		result = self.solver.check()
+		if result == unknown:
+			raise BaseException('Unable to prove rule.')
+		elif result == sat:
+			m = self.solver.model()
+			raise BaseException('Rule is incorrect.\nModel: ' + str(m))
+		self.solver.pop()

test/formal/shl_workaround_8.py

@@ -0,0 +1,27 @@
+from rule import Rule
+from opcodes import *
+
+"""
+Shift left workaround that Solidity implements
+due to a bug in Boost.
+"""
+
+rule = Rule()
+
+n_bits = 8
+bigint_bits = 16
+
+# Input vars
+X = BitVec('X', n_bits)
+A = BitVec('A', n_bits)
+B = BitVec('B', bigint_bits)
+
+# Compute workaround
+workaround = Int2BV(
+	BV2Int(
+		(Int2BV(BV2Int(X), bigint_bits) << Int2BV(BV2Int(A), bigint_bits)) &
+		Int2BV(BV2Int(Int2BV(IntVal(-1), n_bits)), bigint_bits)
+	), n_bits
+)
+
+rule.check(workaround, SHL(A, X))