evm.smt2

;; Proof of concept implementation of a simple stack machine
;; implementing PUSH1, ADD and STOP using the smt 
;; It reads a "codestring", which is translated to opcodes according
;; to the following table:
;; 0 -> STOP
;; 1 -> PUSH1
;; 2 -> ADD
;;
;; It does not deal with integer overflow or with stack overflow
;; but it does handle stack underflow.

;; If you have z3 installed, you can run this file with `z3 evm.smt2`.
;; Since the queries are given the `:print-certificate` tag, this will output
;; a proof trace, which in our case looks very similar to an execution trace.

;; The State record keeps track of the state of the EVM
(declare-datatypes () ((State (mkState
                               (error Bool)
                               (running Bool)
                               (stack (List Int))
                               (stackLength Int)
                               (pc Int)
                               (code (Seq (_ BitVec 8)))
                               )))) ;; and so on...

;; The `state` relation will come to relate instances of `State` through the `rule`s below.
(declare-rel state (State))
(declare-var s State)

;; Some helper variables needed for some functions
(declare-var x Int)
(declare-var y Int)
(declare-var xs (List Int))

;; The semantics are defined with a set of constrained horn clauses (CHC):
(rule ;; PUSH1 (success case)
(=>
 (and
  (state s)
  (running s)
  (= (str.to.int (seq.at (code s) (pc s))) 1)
  (> (seq.len (code s)) (+ (pc s) 1)))
 (state (mkState
         false
         true
         (insert (str.to.int (seq.at (code s) (+ (pc s) 1))) (stack s))
         (+ (stackLength s) 1)
         (+ (pc s) 2)
         (code s)))
 ) PUSH1_SUCCESS)

(rule ;; PUSH1 (error case)
(=>
 (and
  (state s)
  (running s)
  (= (str.to.int (seq.at (code s) (pc s))) 1)
  (<= (seq.len (code s)) (+ (pc s) 1)))
 
 (state (mkState
         true
         false
         (stack s)
         (stackLength s)
         (pc s)
         (code s)))
 ) PUSH1_ERROR)

(rule ;; ADD (success case)
(=>
 (and
  (state s)
  (= (stack s) (insert x (insert y xs)))
  (running s)
  (= (str.to.int (seq.at (code s) (pc s))) 2))
 
  (state (mkState
         false
         true
         (insert 
           (+ x y) xs)
         (- (stackLength s) 1)
         (+ (pc s) 1)
         (code s)))
 )  ADD_SUCCESS
)

(rule ;; ADD (error case)
(=>
 (and
  (state s)
  (running s)
  (= (str.to.int (seq.at (code s) (pc s))) 2)
  (< (stackLength s) 2))
 
 (state (mkState
         true
         false
         (stack s)
         (stackLength s)
         (pc s)
         (code s)))
 ) ADD_ERROR
)

(rule ;; STOP (pc > codesize or code[pc] == 0)
(=>
 (and
  (state s)
  (running s)
  (or (<= (seq.len (code s)) (pc s))
      (= (str.to.int (seq.at (code s) (pc s))) 0)))
 
 (state (mkState
         false
         false
         (stack s)
         (stackLength s)
         (pc s)
         (code s)))
 ) STOP
)

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

;; --- 1 + 2 = 3 ----
(declare-rel stopped1 ())
;; Given the following code:
;; code := PUSH 1 PUSH 2 ADD : 0x0101010202

(rule (state (mkState false true nil 0 0 "11122")))

;; we end up in the following state:

;; error:   false
;; running: false
;; stack:   [3]
;; pc: 5

(rule
 (=> (state (mkState false false (insert 3 nil) 1 5 "11122"))
     stopped1))

(query stopped1 :print-answer true)

;; --- PUSH1: Stack underflow ----
(declare-rel stopped2 ())
;; Given the following code:
;; code := PUSH1: 0x01

(rule (state (mkState false true nil 0 0 "1")))

;; we end up in the following (failing) state:

;; error:   true
;; running: false
;; stack:   []
;; pc: 0

(rule
 (=> (state (mkState true false nil 0 0 "1"))
     stopped2))

(query stopped2 :print-certificate true)

;; --- ADD: Stack underflow ----
(declare-rel stopped3 ())
;; Given the following code:
;; code := ADD: 0x02
(rule (state (mkState false true nil 0 0 "2")))

;; we end up in the following (failing) state:

;; error:   true
;; running: false
;; stack:   []
;; pc: 0
;; 
(rule
 (=> (state (mkState true false nil 0 0 "2"))
     stopped3))

(query stopped3 :print-certificate true)

;; --- 1 + 2 + 3 = 6 ----
(declare-rel stopped4 ())
;; Given the following code:
;; code := PUSH 1 PUSH 2 ADD : 0x0101010202

(rule (state (mkState false true nil 0 0 "11122132")))

;; we end up in the following state:

;; error:   false
;; running: false
;; stack:   [3]
;; pc: 5

(rule
 (=> (state (mkState false false (insert 6 nil) 1 8 "11122132"))
     stopped4))

(query stopped4 :print-answer true)

stack should be 6 and pc 8?
https://gist.github.com/MrChico/6fdbf2f4009bd06d2aecf7e05f675df4#file-evm-smt2-L196-L197