Add FV specification for ERC20Wrapper

[Amxx]

Certora specs for the ERC20 wrapper, rewritten almost from scratch

[changeset-bot]

🦋 Changeset detected

Latest commit: 0c57f1b

The changes in this PR will be included in the next version bump.

This PR includes changesets to release 1 package

Name	Type
openzeppelin-solidity	Minor

Not sure what this means? Click here to learn what changesets are.

Click here if you're a maintainer who wants to add another changeset to this PR

[frangio]

When we specify an invariant, is it only checked for the methods listed in this block? What happens if we add a new function in the Solidity code and we don't add it here?

I just noticed this in the docs and I find it concerning!

It is possible for a method signature to appear in the methods block but not in the contract being verified. In this case, the Prover will skip any rules that mention the missing method, rather than reporting an error.

[Amxx]

AFAIK:

• The invariant (and arbitrary methods) will check all functions in the contract's ABI, even if not here.
• Putting them here allow to mark them envfree, of set a summarize policy
• If a rule does a test on a function declared here, its absence from the contract will not break things and the tests will just be ignored.

[frangio]

Can't we write:

Suggested change

	require underlyingBalanceOf(currentContract) <= underlyingTotalSupply();
	requireInvariant totalSupplyIsSmallerThanUnderlyingBalance;

[Amxx]

since we are in the definition of totalSupplyIsSmallerThanUnderlyingBalance

that would be saying totalSupplyIsSmallerThanUnderlyingBalance holds assuming totalSupplyIsSmallerThanUnderlyingBalance. I hope the prover will reject that. It a bit like using a variable inside its own declaration.

[Amxx]

we could do

sumOfUnderlyingBalancesLowerThanUnderlyingSupply(currentContract, 0);

[frangio]

It a bit like using a variable inside its own declaration.

No, that is not the case according to the docs on invariants. The preserve block is included as a precondition, so by using a "recursive" requireInvariant in its own preserve block, we're just stating that this is an inductive property.

[Amxx]

Isn't the whole point of an invariant that its a precondition of itself?

• [instace] we test that its holds a construction
• [preserve] assuming it holds, execute any function and check that it still holds.

I don't understand what requiring it adds, since its already assumed to hold before the function call