Add Dai Specs

[gbalabasquer]

For commit 6623d372e4164bd879df7b054703add8807d424b, executing:

certoraRun contracts/l2/dai.sol:Dai --verify Dai:contracts/specs/dai.spec --rule_sanity --solc_args "['--optimize','--optimize-runs','200']"

Status page Verification report Full report

[kmbarry1]

In general I like the approach taken here. Separating out the succeed vs revert specs as w/klab is nice. I like the method of exhaustiveness checking in the revert case. Left a number of comments but fundamentally this looks like a great set of patterns to standardize on.

[gbalabasquer]

@kmbarry1 @naszam So I was doing the following test, adding this function to the contract:

function mint2(address to, uint256 value) external auth {
    balanceOf[to] = balanceOf[to] + value;
    totalSupply   = totalSupply + value;
  }

The invariant balanceSum_cant_overflow still passes, which I'm not really sure why. Definitely is not proving what I thought it was proving.

[gbalabasquer]

So balanceSum it is also a uint256, that means that it will also overflow and will never be higher than max_uint256. What we should prove is that the sum of all the balances can't be higher than max_uint256. Not sure if there is a way.

[kmbarry1]

So balanceSum it is also a uint256, that means that it will also overflow and will never be higher than max_uint256. What we should prove is that the sum of all the balances can't be higher than max_uint256. Not sure if there is a way.

That should be theoretically possible since overflow of totalSupply is checked in mint.

But proving just the sum invariant is already pretty powerful because in practice you'll have some finite totalSupply and you'll know you can't get overflows on transfers.

[kmbarry1]

Certora has support for "mathematical integers" that don't overflow as well as EVM-style 256 bit integers:

https://certora.atlassian.net/wiki/spaces/CPD/pages/7340101/Types#EVM-types-vs.-mathematical-types

Might be able to leverage that. E.g. can we make balanceSum() a mathematical integer?

[gbalabasquer]

So balanceSum it is also a uint256, that means that it will also overflow and will never be higher than max_uint256. What we should prove is that the sum of all the balances can't be higher than max_uint256. Not sure if there is a way.

That should be theoretically possible since overflow of totalSupply is checked in mint.

But proving just the sum invariant is already pretty powerful because in practice you'll have some finite totalSupply and you'll know you can't get overflows on transfers.

Yeah not sure why just invoking requireInvariant balanceSum_equals_totalSupply(); on transfer rule doesn't work, the counter example shows a case where the supply is lower than the balances.

[gbalabasquer]

Certora has support for "mathematical integers" that don't overflow as well as EVM-style 256 bit integers:

https://certora.atlassian.net/wiki/spaces/CPD/pages/7340101/Types#EVM-types-vs.-mathematical-types

Might be able to leverage that. E.g. can we make balanceSum() a mathematical integer?

It can actually be defined as mathint. I was playing with it for a while but getting weird stuff. Will keep trying.

[gbalabasquer]

@kmbarry1 @naszam It seems with https://github.com/makerdao/optimism-dai-bridge/pull/45/commits/5bf2e760c0ab6e592102cdc79ad5ebfd19c7dbc5 change I was able to use the invariant to make transfer and transferFrom to pass, and the nice thing is if I add the same mint2 function than before, the invariant shows that this new function breaks it which is what I wanted to prove. I think with this change, now we can assert that there isn't a way in the whole code flow to provoke overflow. Before claiming victory I want further review from both of you and then we can double check it with Shelly.

[naszam]

Ready for a Final Review @kmbarry1 @WilfredTA. cc: @gbalabasquer @hexonaut

• certora-cli >= 2.6.1

  • pip3 install certora-cli==2.6.1

• Switch to solc 0.7.6

  pip3 install solc-select && solc-select install 0.7.6

• Dai

  yarn certora

  Report