Merge pull request #6973 from ethereum/ci_proofs

Add CI job for optimization proofs

.circleci/config.yml

@@ -33,6 +33,9 @@ defaults:
       command: |
         export ASAN_OPTIONS="check_initialization_order=true:detect_stack_use_after_return=true:strict_init_order=true:strict_string_checks=true:detect_invalid_pointer_pairs=2"
         scripts/regressions.py -o test_results
+  - run_proofs: &run_proofs
+      name: Correctness proofs for optimization rules
+      command: scripts/run_proofs.sh
   - solc_artifact: &solc_artifact
       path: build/solc/solc
       destination: solc
@@ -304,6 +307,21 @@ jobs:
           name: Test buglist
           command: ./test/buglistTests.js
 
+  proofs:
+    docker:
+      - image: buildpack-deps:bionic
+    environment:
+      TERM: xterm
+    steps:
+      - checkout
+      - run:
+          name: Z3 python deps
+          command: |
+            apt-get -qq update
+            apt-get -qy install python-pip
+            pip install --user z3-solver
+      - run: *run_proofs
+
   test_x86_linux:
     docker:
       - image: buildpack-deps:bionic
@@ -490,6 +508,7 @@ workflows:
       - test_check_spelling: *build_on_tags
       - test_check_style: *build_on_tags
       - test_buglist: *build_on_tags
+      - proofs: *build_on_tags
       - build_emscripten: *build_on_tags
       - test_emscripten_solcjs:
           <<: *build_on_tags

scripts/run_proofs.sh

@@ -0,0 +1,29 @@
+#!/usr/bin/env bash
+
+set -e
+
+REPO_ROOT="$(dirname "$0")"/..
+
+git fetch origin
+error=0
+for new_proof in $(git diff develop --name-only $REPO_ROOT/test/formal/)
+do
+	set +e
+	echo "Proving $new_proof..."
+	output=$(python "$REPO_ROOT/$new_proof")
+	result=$?
+	set -e
+
+	if [[ "$result" != 0 ]]
+	then
+		echo "Proof $(basename "$new_proof" ".py") failed: $output."
+		error=1
+	fi
+done
+
+if [[ "error" -eq 0 ]]
+then
+	echo "All proofs succeeded."
+fi
+
+exit $error

test/formal/rule.py

@@ -1,3 +1,5 @@
+import sys
+
 from z3 import *
 
 class Rule:
@@ -21,9 +23,9 @@ class Rule:
 		result = self.solver.check()
 
 		if result == unknown:
-			raise BaseException('Unable to satisfy requirements.')
+			self.error('Unable to satisfy requirements.')
 		elif result == unsat:
-			raise BaseException('Requirements are unsatisfiable.')
+			self.error('Requirements are unsatisfiable.')
 
 		self.solver.push()
 		self.solver.add(self.constraints)
@@ -31,8 +33,12 @@ class Rule:
 
 		result = self.solver.check()
 		if result == unknown:
-			raise BaseException('Unable to prove rule.')
+			self.error('Unable to prove rule.')
 		elif result == sat:
 			m = self.solver.model()
-			raise BaseException('Rule is incorrect.\nModel: ' + str(m))
+			self.error('Rule is incorrect.\nModel: ' + str(m))
 		self.solver.pop()
+
+	def error(self, msg):
+		print(msg)
+		sys.exit(1)