Merge pull request #6944 from ethereum/checkedArithmeticProofs

Proofs for the correctness of overflow checks in Sol->Yul code generation.

scripts/run_proofs.sh

@@ -2,15 +2,17 @@
 
 set -e
 
+(
 REPO_ROOT="$(dirname "$0")"/..
+cd "$REPO_ROOT"
 
 git fetch origin
 error=0
-for new_proof in $(git diff develop --name-only $REPO_ROOT/test/formal/)
+for new_proof in $(git diff origin/develop --name-only test/formal/)
 do
 	set +e
 	echo "Proving $new_proof..."
-	output=$(python "$REPO_ROOT/$new_proof")
+	output=$(python "$new_proof")
 	result=$?
 	set -e
 
@@ -27,3 +29,4 @@ then
 fi
 
 exit $error
+)

test/formal/checked_int_add.py

@@ -0,0 +1,39 @@
+from rule import Rule
+from opcodes import *
+from util import *
+
+"""
+Overflow checked signed integer addition.
+"""
+
+n_bits = 256
+type_bits = 8
+
+while type_bits <= n_bits:
+
+	rule = Rule()
+
+	# Input vars
+	X_short = BitVec('X', type_bits)
+	Y_short = BitVec('Y', type_bits)
+
+	# Z3's overflow and underflow conditions
+	actual_overflow = Not(BVAddNoOverflow(X_short, Y_short, True))
+	actual_underflow = Not(BVAddNoUnderflow(X_short, Y_short))
+
+	# cast to full n_bits values
+	X = BVSignedUpCast(X_short, n_bits)
+	Y = BVSignedUpCast(Y_short, n_bits)
+
+	# Constants
+	maxValue = BVSignedMax(type_bits, n_bits)
+	minValue = BVSignedMin(type_bits, n_bits)
+
+	# Overflow and underflow checks in YulUtilFunction::overflowCheckedIntAddFunction
+	overflow_check = AND(ISZERO(SLT(X, 0)), SGT(Y, SUB(maxValue, X)))
+	underflow_check = AND(SLT(X, 0), SLT(Y, SUB(minValue, X)))
+
+	rule.check(actual_overflow, overflow_check != 0)
+	rule.check(actual_underflow, underflow_check != 0)
+
+	type_bits *= 2

test/formal/checked_int_div.py

@@ -0,0 +1,35 @@
+from rule import Rule
+from opcodes import *
+from util import *
+
+"""
+Overflow checked signed integer division.
+"""
+
+n_bits = 256
+type_bits = 8
+
+while type_bits <= n_bits:
+
+	rule = Rule()
+
+	# Input vars
+	X_short = BitVec('X', type_bits)
+	Y_short = BitVec('Y', type_bits)
+
+	# Z3's overflow conditions
+	actual_overflow = Not(BVSDivNoOverflow(X_short, Y_short))
+
+	# cast to full n_bits values
+	X = BVSignedUpCast(X_short, n_bits)
+	Y = BVSignedUpCast(Y_short, n_bits)
+
+	# Constants
+	minValue = BVSignedMin(type_bits, n_bits)
+
+	# Overflow check in YulUtilFunction::overflowCheckedIntDivFunction
+	overflow_check = AND(EQ(X, minValue), EQ(Y, SUB(0, 1)))
+
+	rule.check(actual_overflow, overflow_check != 0)
+
+	type_bits *= 2

test/formal/checked_int_mul_16.py

@@ -0,0 +1,42 @@
+from rule import Rule
+from opcodes import *
+from util import *
+
+"""
+Overflow checked signed integer multiplication.
+"""
+
+# Approximation with 16-bit base types.
+n_bits = 16
+type_bits = 8
+
+while type_bits <= n_bits:
+
+	rule = Rule()
+
+	# Input vars
+	X_short = BitVec('X', type_bits)
+	Y_short = BitVec('Y', type_bits)
+
+	# Z3's overflow and underflow conditions
+	actual_overflow = Not(BVMulNoOverflow(X_short, Y_short, True))
+	actual_underflow = Not(BVMulNoUnderflow(X_short, Y_short))
+
+	# cast to full n_bits values
+	X = BVSignedUpCast(X_short, n_bits)
+	Y = BVSignedUpCast(Y_short, n_bits)
+
+	# Constants
+	maxValue = BVSignedMax(type_bits, n_bits)
+	minValue = BVSignedMin(type_bits, n_bits)
+
+	# Overflow and underflow checks in YulUtilFunction::overflowCheckedIntMulFunction
+	overflow_check_1 = AND(AND(SGT(X, 0), SGT(Y, 0)), GT(X, DIV(maxValue, Y)))
+	underflow_check_1 = AND(AND(SGT(X, 0), SLT(Y, 0)), SLT(Y, SDIV(minValue, X)))
+	underflow_check_2 = AND(AND(SLT(X, 0), SGT(Y, 0)), SLT(X, SDIV(minValue, Y)))
+	overflow_check_2 = AND(AND(SLT(X, 0), SLT(Y, 0)), SLT(X, SDIV(maxValue, Y)))
+
+	rule.check(actual_overflow, Or(overflow_check_1 != 0, overflow_check_2 != 0))
+	rule.check(actual_underflow, Or(underflow_check_1 != 0, underflow_check_2 != 0))
+
+	type_bits *= 2

test/formal/checked_int_sub.py

@@ -0,0 +1,39 @@
+from rule import Rule
+from opcodes import *
+from util import *
+
+"""
+Overflow checked signed integer subtraction.
+"""
+
+n_bits = 256
+type_bits = 8
+
+while type_bits <= n_bits:
+
+	rule = Rule()
+
+	# Input vars
+	X_short = BitVec('X', type_bits)
+	Y_short = BitVec('Y', type_bits)
+
+	# Z3's overflow and underflow conditions
+	actual_overflow = Not(BVSubNoOverflow(X_short, Y_short))
+	actual_underflow = Not(BVSubNoUnderflow(X_short, Y_short, True))
+
+	# cast to full n_bits values
+	X = BVSignedUpCast(X_short, n_bits)
+	Y = BVSignedUpCast(Y_short, n_bits)
+
+	# Constants
+	maxValue = BVSignedMax(type_bits, n_bits)
+	minValue = BVSignedMin(type_bits, n_bits)
+
+	# Overflow and underflow checks in YulUtilFunction::overflowCheckedIntSubFunction
+	underflow_check = AND(ISZERO(SLT(Y, 0)), SLT(X, ADD(minValue, Y)))
+	overflow_check = AND(SLT(Y, 0), SGT(X, ADD(maxValue, Y)))
+
+	rule.check(actual_underflow, underflow_check != 0)
+	rule.check(actual_overflow, overflow_check != 0)
+
+	type_bits *= 2

test/formal/checked_uint_add.py

@@ -0,0 +1,35 @@
+from rule import Rule
+from opcodes import *
+from util import *
+
+"""
+Overflow checked unsigned integer addition.
+"""
+
+n_bits = 256
+type_bits = 8
+
+while type_bits <= n_bits:
+
+	rule = Rule()
+
+	# Input vars
+	X_short = BitVec('X', type_bits)
+	Y_short = BitVec('Y', type_bits)
+
+	# Z3's overflow condition
+	actual_overflow = Not(BVAddNoOverflow(X_short, Y_short, False))
+
+	# cast to full n_bits values
+	X = BVUnsignedUpCast(X_short, n_bits)
+	Y = BVUnsignedUpCast(Y_short, n_bits)
+
+	# Constants
+	maxValue = BVUnsignedMax(type_bits, n_bits)
+
+	# Overflow check in YulUtilFunction::overflowCheckedIntAddFunction
+	overflow_check = GT(X, SUB(maxValue, Y))
+
+	rule.check(overflow_check != 0, actual_overflow)
+
+	type_bits *= 2

test/formal/checked_uint_mul_16.py

@@ -0,0 +1,36 @@
+from rule import Rule
+from opcodes import *
+from util import *
+
+"""
+Overflow checked unsigned integer multiplication.
+"""
+
+# Approximation with 16-bit base types.
+n_bits = 16
+type_bits = 8
+
+while type_bits <= n_bits:
+
+	rule = Rule()
+
+	# Input vars
+	X_short = BitVec('X', type_bits)
+	Y_short = BitVec('Y', type_bits)
+
+	# Z3's overflow condition
+	actual_overflow = Not(BVMulNoOverflow(X_short, Y_short, False))
+
+	# cast to full n_bits values
+	X = BVUnsignedUpCast(X_short, n_bits)
+	Y = BVUnsignedUpCast(Y_short, n_bits)
+
+	# Constants
+	maxValue = BVUnsignedMax(type_bits, n_bits)
+
+	# Overflow check in YulUtilFunction::overflowCheckedIntMulFunction
+	overflow_check = AND(ISZERO(ISZERO(X)), GT(Y, DIV(maxValue, X)))
+
+	rule.check(overflow_check != 0, actual_overflow)
+
+	type_bits *= 2

test/formal/checked_uint_sub.py

@@ -0,0 +1,35 @@
+from rule import Rule
+from opcodes import *
+from util import *
+
+"""
+Overflow checked unsigned integer subtraction.
+"""
+
+n_bits = 256
+type_bits = 8
+
+while type_bits <= n_bits:
+
+	rule = Rule()
+
+	# Input vars
+	X_short = BitVec('X', type_bits)
+	Y_short = BitVec('Y', type_bits)
+
+	# Z3's overflow condition
+	actual_overflow = Not(BVSubNoUnderflow(X_short, Y_short, False))
+
+	# cast to full n_bits values
+	X = BVUnsignedUpCast(X_short, n_bits)
+	Y = BVUnsignedUpCast(Y_short, n_bits)
+
+	# Constants
+	maxValue = BVUnsignedMax(type_bits, n_bits)
+
+	# Overflow check in YulUtilFunction::overflowCheckedIntSubFunction
+	overflow_check = LT(X, Y)
+
+	rule.check(overflow_check != 0, actual_overflow)
+
+	type_bits *= 2

test/formal/opcodes.py

@@ -33,6 +33,9 @@ def SLT(x, y):
 def SGT(x, y):
 	return If(x > y, BitVecVal(1, x.size()), BitVecVal(0, x.size()))
 
+def EQ(x, y):
+	return If(x == y, BitVecVal(1, x.size()), BitVecVal(0, x.size()))
+
 def ISZERO(x):
 	return If(x == 0, BitVecVal(1, x.size()), BitVecVal(0, x.size()))
 

test/formal/util.py

@@ -0,0 +1,27 @@
+from z3 import *
+
+def BVUnsignedUpCast(x, n_bits):
+	assert(x.size() <= n_bits)
+	if x.size() < n_bits:
+		return Concat(BitVecVal(0, n_bits - x.size()), x)
+	else:
+		return x
+
+def BVUnsignedMax(type_bits, n_bits):
+	assert(type_bits <= n_bits)
+	return BitVecVal((1 << type_bits) - 1, n_bits)
+
+def BVSignedUpCast(x, n_bits):
+	assert(x.size() <= n_bits)
+	if x.size() < n_bits:
+		return Concat(If(x < 0, BitVecVal(-1, n_bits - x.size()), BitVecVal(0, n_bits - x.size())), x)
+	else:
+		return x
+
+def BVSignedMax(type_bits, n_bits):
+	assert(type_bits <= n_bits)
+	return BitVecVal((1 << (type_bits - 1)) - 1, n_bits)
+
+def BVSignedMin(type_bits, n_bits):
+	assert(type_bits <= n_bits)
+	return BitVecVal(-(1 << (type_bits - 1)), n_bits)