feat: more flexible/powerful ways to define and test invariants

[mds1]

Component

Forge

Describe the feature you would like

This is an idea / open for discussion, feedback encouraged.

Some invariants are hard to specify with the current UX, such as "only calls from <addressX> are allowed to modify the allowance[addressX][spender] mapping". I haven't thought of a way to enable things like this without a preprocessor/domain-specific language, so here is one proposal to test for things like this.

A modifier-like behavior for storage variables could allow this, i.e. solidity code that executes before and after a given slot is touched to verify some property of that slot. For example, below we use a comment to annotate the balanceOf function, which tells forge to run the verifyBalanceOf method before/after a slot in that mapping is changed. In our test contract, we can see that definition: it checks the start and end balance of the user. If balance decreased, make sure the required conditions for modification have been met.

contract Token {
  /// @invariant verifyBalanceOf
  mapping(address => uint256) public balanceOf;

  // -- snip --
}

contract TokenTest is Token {
  // Since this is testing a mapping, we have one input which is the mapping key
  modifier verifyBalanceOf(address user) public {
    uint256 startBalance = balanceOf(user);
    _;
    uint256 endBalance = balanceOf(user);
    if (endBalance < startBalance) {
      // balance decreased, ensure this was authorized
      assert(msg.sender == user || allowances[user][msg.sender] >= startBalance - endBalance);
    }
  }
}

Additional context

No response