SMT: Detect Collisions in Mapping Assignments

[d-xo]

In order for the properties proven against an act spec to be sound, it is important that the updates to elements in storage mappings cannot collide or overlap.

As an example, the following spec is invalid as it is possible for usr and CALLER to have the same value:

constructor of Broken
interface constructor()

creates

    mapping (address => (mapping address => uint)) a := []

behaviour whoops of Broken
interface whoops(address usr1, address usr2)

storage

    a[usr1][CALLER] => 10
    a[CALLER][usr2] => 9

We can define an automated analysis backed by an SMT solver that will detect these issues. First we need to extract every pair of storagelocations that refer to the same mapping. For each of these pairs we then ask the solver to find a satisfying assignment of values so that each pair of elements at each index position are equal.

In the case of the example above this would look something like the following smt (we should of course also assert any preconditions in the behaviour):

(declare-const usr1 Int)
(declare-const usr2 Int)
(declare-const caller Int)

(assert (and (= usr1 caller) (= caller usr2)))
(check-sat)

A result of unsat constitutes a proof that each of the locations is disjoint in all possible states.