Contract invariants are properties that we expect to be maintained by the contract at 'all times'.

Invariant example: "The total of all balances doesn't change"

Contract invariants in Scribble are similar to class invariants in object oriented languages - internal functions to the contract are allowed to temporarily violate the invariants. However whenever we "exit" the contract (by either returning from an external call into it, or by making an external call from it), the invariants must be true. We refer to these points in the execution as places where the state is externally observable.

Observable State

The state of a contract is observable whenever some external contract can read it.

before call (observable): The state of a contract before executing a transaction is observable! At this point anyone, and any contract could read and call into a contract. Those callers / readers expect the invariant to hold.

during call (not-observable): During a contract's execution nobody looks at the state of the contract. So it's fine if an invariant doesn't hold at this point.

before making external call out (observable): If we call to another contract, then that contract can read our state or call back. This external contract expects the invariant to hold!

after (returning from) external call (observable): Once a contract is finished executing we are back to a scenario where anyone and any contract can read and call into our state. So, the invariant should hold again at this point.

Example Observability

Let's explore an example. The invariant we'll use is "the variable x is 0"

/// #invariant {:msg "the variable x is 0"} x == 0;
contract Example {
    // Good, x holds in the beginning
    uint public x = 0;
​
    function example_observability() {
        // x should be 0 here
        x *= 10;
        // x is still 0 if x was zero
        return;
        // x is still zero if x was zero, great!
    }
​
    function example_violation() {
        // x should be 0 here
        x += 1;
        return;
        // x is not zero anymore 😢
        // now the invariant is violated 
    }
​
​
    function example_nonviolation() {
        // x should be 0 here
        x += 1;
        // Now x is non zero, but that doesn't matter. We're not "observable".
        x -= 1;
        // We immediately return x back to what it was
        return;
        // x is back to zero again (if it was zero before)!
    }
​
    function example_external(address externalContract) {
        // x should be 0 here
        x += 1;
        // Now x is non zero. Which violates the invariant.
        externalContract.call();
​
        // externalContract might call back into us, assuming that the invariant holds
        // For example:
        // If externalContract calls this.example_observability(), expecting all invariants to hold.
        // Unfortunately, x is not 0. example_observability()'s assumption is violated.
​
        return;
    }
​
}

Syntax

Invariants have the following structure, and are placed above contract declarations:

invariant {:msg "<Description of your property>"} <boolean scribble expression>;

/// #invariant {:msg "The total balance doesn't change."} totalBalance == old(totalBalance);
contract ExampleContract {
​
}

/// #invariant {:msg "Only the owner changes the owner"} owner != old(owner) ==> msg.sender == old(owner);
contract ExampleContract {
    address public owner;
}

External Calls

There are two kinds of external calls: Ones that call to this and ones that call into other contracts.

Scribble asserts that an invariant is valid at the end of contract construction, as this is the first point where contract state becomes observable. However, due to the mechanics of the EVM the contract account is not 100% set up. Calls into the contract don't work yet, because there is not actually any code at the contract address until the constructor returns. This is why you can't use re-entrant calls like this.getTotalBalance() in a contract invariant.

The second type of external call, those to other contracts, is possible with Scribble. But we consider this an anti-pattern.

Invariants are meant to describe properties that must always hold for a single contract. We write properties for the contract in isolation, agnostic of any external components. This makes testing more efficient and reflects the composability of (DeFi) smart contracts.