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

[PaulRBerg]

This is an interesting proposal, but just so I understand it correctly, is the idea to annotate the production contract with this sort of comment?

/// @invariant verifyBalanceOf

Or some wrapper test contract that is used only when testing invariants?

[mds1]

The intent was to annotate the production contract, just because it seems a lot cleaner/simpler. There is some precedent for this, e.g. slither and scribble support using custom comments to convey info to them. Totally open to alternative UX here though

[PaulRBerg]

I see, thanks for confirming.

In this case, I will make a similar proposal to that made in #4085, which is to use the NatSpec prefix @custom::

/// @custom:invariant verifyBalanceOf

Might be slightly more verbose but if my understanding of NatSpec is right, typing it out like this would include the name of the invariant in the contract ABI.

[mds1]

Main downside there is you need at least solidity 0.8.2, otherwise I believe compilation fails due to invalid natspec tag (probably the same issue with my original syntax). We'd want a custom comment syntax, e.g. slither uses //slither-disable-next-line DETECTOR_NAME, perhaps something like // forge-invariant to mirror the supported // forgefmt syntax

[PaulRBerg]

argh, shoot, wasn't aware that compilation fails prior to 0.8.2!

Custom comment syntax should be fine, though.