Aliasing and Unique Ownership

In order to reason about smart contracts in a purely functional way, we leverage the concept of unique ownership. This means that each contract has a single owner, and there are no shared references to the contract's state. This simplifies reasoning about state changes and ensures that contracts cannot inadvertently interfere with each other.

We showcase an issue with aliasing in the following example: suppose we have a contract A that contains two storage variables that contain an ERC20 token: Token t0 and Token t1.

contract A 
    constructor(address<Token> a0, address<Token> a1) 
        creates 
            Token t0 := a0
            Token t1 := a1
    transition transfer (uint256 _value, address to)
        updates 
            t0.balanceOf := t0.balanceOf[CALLER => t0.balanceOf[CALLER] - _value]
            t1.balanceOf := t1.balanceOf[to => t1.balanceOf[to] + _value]

To reason about the contract A in Rocq in a purely functional way, we would map the contract to a Rocq record of type

Record State := {t0: Token.State; t1: Token.State}

In this example, if a0 and a1 point to the same ERC20 Token contract, then the transfer transition update of t0.balanceOf will also affect t1.balanceOf, breaking the functional abstraction we want to achieve (namely modifying only the t0 field in the record).

However, if we can prove that t0 and t1 can never alias then we can safely reason about their state changes independently. Note that including an iff address(a0) != address(a1) condition in the constructor's preconditions is required, but not sufficient, as the Token contract itself also needs to avoid aliasing. But since we also have the Token contract specification ready, act will verify the unique ownership property also for that.

This unique ownership property is verified automatically for act specifications using symbolic execution and SMT solving. Note that the unique ownership property is not an implicit check in act, but rather an implicit assumption, which is then check to hold in the post-state, to make sure it is upheld as an invariant.