evm_chc.smt2

;;------------- State definition ---------
(declare-datatypes () ((State (mkState (error Bool) (running Bool) (stack (Array Int Int)) (len Int) ))))

;;------------- Opcode declarations ------------

(declare-rel evmPush (State Int State))
(declare-rel evmAdd (State State))
(declare-rel evmStop (State State))

;;------------- Helper vars --------------
(declare-var s State)
(declare-var x Int)
(declare-var y Int)
(declare-var lenPost Int)
(declare-var stackPost (Array Int Int))
(declare-var sPost State)

;;------------- Execution -----------
(declare-rel contractBegin (State))


;;------------- Query helpers ------------

(declare-rel stopped ())
(declare-rel stopped_error ())

;;------------- Opcodes semantics ------------

(rule ;; PUSH1
(=>
	(and
		(running s)
		(= lenPost (+ (len s) 1))
		(= stackPost (store (stack s) (len s) x))
		(= sPost (mkState false true stackPost lenPost))
	)
	(evmPush s x sPost)
))

(rule ;; ADD (success case)
(=>
	(and
		(running s)
		(>= (len s) 2)
		(= lenPost (- (len s) 1))
		(= x (select (stack s) (- (len s) 1)))
		(= y (select (stack s) (- (len s) 2)))
		(= stackPost (store (stack s) (- lenPost 1) (+ x y)))
		(= sPost (mkState false true stackPost lenPost))
	)
	(evmAdd s sPost)
))

(rule ;; ADD (error case)
(=>
	(and
		(running s)
		(< (len s) 2)
		(= sPost (mkState true false (stack s) (len s)))
	)
	(evmAdd s sPost)
))

(rule ;; STOP
(=>
	(and
		(running s)
		(= sPost (mkState false false (stack s) (len s)))
	)
	(evmStop s sPost)
))

;;------------- Execution -------------------

(rule ;; MAIN: Contract's entry point
(=>
	(and
		(running s)
		(not (error s))
		(= (len s) 0)
	)
	(contractBegin s)
))

;;------------- tests ------------

;; --- 1 + 2 = 3 ----
;;; Given the following code:
;;; code := PUSH 1 PUSH 2 ADD : 0x0101010202
;

(declare-rel contractEndTest1 (State))
(declare-rel block2 (State))
(declare-rel block3 (State))
(declare-rel block4 (State))

(rule
(=>
	(and
		(contractBegin s)
		(evmPush s 1 sPost)
	)
	(block2 sPost)
))

(rule
(=>
	(and
		(block2 s)
		(evmPush s 2 sPost)
	)
	(block3 sPost)
))

(rule
(=>
	(and
		(block3 s)
		(evmAdd s sPost)
	)
	(block4 sPost)
))

(rule
(=>
	(block4 s)
	(contractEndTest1 s)
))

(rule
(=>
	(and
		(contractEndTest1 s)
		(= x (select (stack s) (- (len s) 1)))
		(not (= x 3))
	)
	stopped_error
))

;
;;; we end up in the following state:
;
;;; error:   false
;;; running: false
;;; stack:   [3]
;
(query stopped_error :print-certificate true)