What is a minimal symbolic execution example?

Question

I'd like to see a minimal symbolic execution / formal verification example using the following function:

function f(uint256 a) public returns(uint256){
  a = a + 1;
  return a;
}

What would that look like?

Answer 1

When we look at this function, we can easily see two paths this function can take.

1. a < 2^256, a = a + 1, function returns
2. a == 2^256, a = a + 1 overflows, function reverts

We can turn these into a set of boolean expressions. Then, input those into a SAT Solver with some "question" added to it. We can see what this code would look like in SMT-LIB format to input to something like the z3 SMT Solvet.

; Declare a symbolic integer variable 'a' as a 256-bit integer
(declare-const a (_ BitVec 256))

; Create a context for Path 1
(push)

; Add assertions for Path 1
; assert a is not equal to `uint256.max`
(assert (distinct a #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff))
(check-sat)

; Remove the context for Path 1
(pop)

; Create a context for Path 2
(push)

; Add assertions for Path 2
; assert a is equal to `uint256.max`
(assert (= a #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff))
; bvult is "bit vector unsigned less than", so we are checking that a + 1 is less than a
(assert (bvult (bvadd a (_ bv1 256)) a))

; Check if Path 2 is satisfiable
(check-sat)

The (check-sat) line is sort of the "question" we are asking. We are saying "is there a variable a such that all the booleans in this list are true?"

If the property of our smart contract was "f should never revert" we could see Path 2 holds that "question".

This line:

(assert (bvult (bvadd a (_ bv1 256)) a))

Is a boolean saying essentially (a + 1 > a). Since we have included it, you could argue the question we are asking our theorem solver is "with these constraints, could function f ever revert?"

The output of this in z3 would be the following:

sat

Meaning, that yes, the function f could revert.

The hard part of all this, is converting your solidity -> SMT-LIB for a solver solver to digest. Tools like manticore can do this, but will give you the SMT-LIB for the entire contract. ChatGPT can also help create these conversions. It can be really tricky to get this conversion correct though.