Add FV specification for ERC20Wrapper (#4100)

Co-authored-by: Francisco <fg@frang.io>

.changeset/tender-needles-dance.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': minor
+---
+
+`ERC20Wrapper`: self wrapping and deposit by the wrapper itself are now explicitelly forbiden.

certora/harnesses/ERC20PermitHarness.sol

@@ -2,10 +2,9 @@
 
 pragma solidity ^0.8.0;
 
-import "../patched/token/ERC20/ERC20.sol";
 import "../patched/token/ERC20/extensions/ERC20Permit.sol";
 
-contract ERC20PermitHarness is ERC20, ERC20Permit {
+contract ERC20PermitHarness is ERC20Permit {
     constructor(string memory name, string memory symbol) ERC20(name, symbol) ERC20Permit(name) {}
 
     function mint(address account, uint256 amount) external {

certora/harnesses/ERC20WrapperHarness.sol

@@ -0,0 +1,25 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../patched/token/ERC20/extensions/ERC20Wrapper.sol";
+
+contract ERC20WrapperHarness is ERC20Wrapper {
+    constructor(IERC20 _underlying, string memory _name, string memory _symbol) ERC20(_name, _symbol) ERC20Wrapper(_underlying) {}
+
+    function underlyingTotalSupply() public view returns (uint256) {
+        return underlying().totalSupply();
+    }
+
+    function underlyingBalanceOf(address account) public view returns (uint256) {
+        return underlying().balanceOf(account);
+    }
+
+    function underlyingAllowanceToThis(address account) public view returns (uint256) {
+        return underlying().allowance(account, address(this));
+    }
+
+    function recover(address account) public returns (uint256) {
+        return _recover(account);
+    }
+}

certora/run.js

@@ -31,7 +31,7 @@ if (request) {
 }
 
 for (const { spec, contract, files, options = [] } of Object.values(specs)) {
-  limit(runCertora, spec, contract, files, [...options, ...extraOptions]);
+  limit(runCertora, spec, contract, files, [...options.flatMap(opt => opt.split(' ')), ...extraOptions]);
 }
 
 // Run certora, aggregate the output and print it at the end
@@ -50,7 +50,7 @@ async function runCertora(spec, contract, files, options = []) {
     const urls = data.toString('utf8').match(/https?:\S*/g);
     for (const url of urls ?? []) {
       if (url.includes('/jobStatus/')) {
-        console.error(`[${spec}] ${url}`);
+        console.error(`[${spec}] ${url.replace('/jobStatus/', '/output/')}`);
         stream.off('data', logStatusUrl);
         break;
       }
@@ -108,8 +108,8 @@ function writeEntry(spec, contract, success, url) {
       spec,
       contract,
       success ? ':x:' : ':heavy_check_mark:',
-      `[link](${url})`,
+      url ? `[link](${url})` : 'error',
-      `[link](${url?.replace('/jobStatus/', '/output/')})`,
+      url ? `[link](${url?.replace('/jobStatus/', '/output/')})` : 'error',
     ),
   );
 }

certora/specs.json

@@ -29,6 +29,18 @@
     ],
     "options": ["--optimistic_loop"]
   },
+  {
+    "spec": "ERC20Wrapper",
+    "contract": "ERC20WrapperHarness",
+    "files": [
+      "certora/harnesses/ERC20PermitHarness.sol",
+      "certora/harnesses/ERC20WrapperHarness.sol"
+    ],
+    "options": [
+      "--link ERC20WrapperHarness:_underlying=ERC20PermitHarness",
+      "--optimistic_loop"
+    ]
+  },
   {
     "spec": "Initializable",
     "contract": "InitializableHarness",

certora/specs/ERC20Wrapper.spec

@@ -0,0 +1,198 @@
+import "helpers.spec"
+import "ERC20.spec"
+
+methods {
+    underlying()                       returns(address) envfree
+    underlyingTotalSupply()            returns(uint256) envfree
+    underlyingBalanceOf(address)       returns(uint256) envfree
+    underlyingAllowanceToThis(address) returns(uint256) envfree
+
+    depositFor(address, uint256)       returns(bool)
+    withdrawTo(address, uint256)       returns(bool)
+    recover(address)                   returns(uint256)
+}
+
+use invariant totalSupplyIsSumOfBalances
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Helper: consequence of `totalSupplyIsSumOfBalances` applied to underlying                                           │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+function underlyingBalancesLowerThanUnderlyingSupply(address a) returns bool {
+    return underlyingBalanceOf(a) <= underlyingTotalSupply();
+}
+
+function sumOfUnderlyingBalancesLowerThanUnderlyingSupply(address a, address b) returns bool {
+    return a != b => underlyingBalanceOf(a) + underlyingBalanceOf(b) <= underlyingTotalSupply();
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: wrapped token can't be undercollateralized (solvency of the wrapper)                                     │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant totalSupplyIsSmallerThanUnderlyingBalance()
+    totalSupply() <= underlyingBalanceOf(currentContract) &&
+    underlyingBalanceOf(currentContract) <= underlyingTotalSupply() &&
+    underlyingTotalSupply() <= max_uint256
+    {
+        preserved {
+            requireInvariant totalSupplyIsSumOfBalances;
+            require underlyingBalancesLowerThanUnderlyingSupply(currentContract);
+        }
+        preserved depositFor(address account, uint256 amount) with (env e) {
+            require sumOfUnderlyingBalancesLowerThanUnderlyingSupply(e.msg.sender, currentContract);
+        }
+    }
+
+invariant noSelfWrap()
+    currentContract != underlying()
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: depositFor liveness and effects                                                                               │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule depositFor(env e) {
+    require nonpayable(e);
+
+    address sender = e.msg.sender;
+    address receiver;
+    address other;
+    uint256 amount;
+
+    // sanity
+    requireInvariant noSelfWrap;
+    requireInvariant totalSupplyIsSumOfBalances;
+    requireInvariant totalSupplyIsSmallerThanUnderlyingBalance;
+    require sumOfUnderlyingBalancesLowerThanUnderlyingSupply(currentContract, sender);
+
+    uint256 balanceBefore                   = balanceOf(receiver);
+    uint256 supplyBefore                    = totalSupply();
+    uint256 senderUnderlyingBalanceBefore   = underlyingBalanceOf(sender);
+    uint256 senderUnderlyingAllowanceBefore = underlyingAllowanceToThis(sender);
+    uint256 wrapperUnderlyingBalanceBefore  = underlyingBalanceOf(currentContract);
+    uint256 underlyingSupplyBefore          = underlyingTotalSupply();
+
+    uint256 otherBalanceBefore              = balanceOf(other);
+    uint256 otherUnderlyingBalanceBefore    = underlyingBalanceOf(other);
+
+    depositFor@withrevert(e, receiver, amount);
+    bool success = !lastReverted;
+
+    // liveness
+    assert success <=> (
+        sender   != currentContract               && // invalid sender
+        sender   != 0                             && // invalid sender
+        receiver != 0                             && // invalid receiver
+        amount   <= senderUnderlyingBalanceBefore && // deposit doesn't exceed balance
+        amount   <= senderUnderlyingAllowanceBefore  // deposit doesn't exceed allowance
+    );
+
+    // effects
+    assert success => (
+        balanceOf(receiver) == balanceBefore + amount &&
+        totalSupply() == supplyBefore + amount &&
+        underlyingBalanceOf(currentContract) == wrapperUnderlyingBalanceBefore + amount &&
+        underlyingBalanceOf(sender) == senderUnderlyingBalanceBefore - amount
+    );
+
+    // no side effect
+    assert underlyingTotalSupply() == underlyingSupplyBefore;
+    assert balanceOf(other)           != otherBalanceBefore           => other == receiver;
+    assert underlyingBalanceOf(other) != otherUnderlyingBalanceBefore => (other == sender || other == currentContract);
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: withdrawTo liveness and effects                                                                               │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule withdrawTo(env e) {
+    require nonpayable(e);
+
+    address sender = e.msg.sender;
+    address receiver;
+    address other;
+    uint256 amount;
+
+    // sanity
+    requireInvariant noSelfWrap;
+    requireInvariant totalSupplyIsSumOfBalances;
+    requireInvariant totalSupplyIsSmallerThanUnderlyingBalance;
+    require sumOfUnderlyingBalancesLowerThanUnderlyingSupply(currentContract, receiver);
+
+    uint256 balanceBefore                   = balanceOf(sender);
+    uint256 supplyBefore                    = totalSupply();
+    uint256 receiverUnderlyingBalanceBefore = underlyingBalanceOf(receiver);
+    uint256 wrapperUnderlyingBalanceBefore  = underlyingBalanceOf(currentContract);
+    uint256 underlyingSupplyBefore          = underlyingTotalSupply();
+
+    uint256 otherBalanceBefore              = balanceOf(other);
+    uint256 otherUnderlyingBalanceBefore    = underlyingBalanceOf(other);
+
+    withdrawTo@withrevert(e, receiver, amount);
+    bool success = !lastReverted;
+
+    // liveness
+    assert success <=> (
+        sender   != 0          && // invalid sender
+        receiver != 0          && // invalid receiver
+        amount   <= balanceBefore // withdraw doesn't exceed balance
+    );
+
+    // effects
+    assert success => (
+        balanceOf(sender) == balanceBefore - amount &&
+        totalSupply() == supplyBefore - amount &&
+        underlyingBalanceOf(currentContract) == wrapperUnderlyingBalanceBefore - (currentContract != receiver ? amount : 0) &&
+        underlyingBalanceOf(receiver) == receiverUnderlyingBalanceBefore + (currentContract != receiver ? amount : 0)
+    );
+
+    // no side effect
+    assert underlyingTotalSupply() == underlyingSupplyBefore;
+    assert balanceOf(other)           != otherBalanceBefore           => other == sender;
+    assert underlyingBalanceOf(other) != otherUnderlyingBalanceBefore => (other == receiver || other == currentContract);
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: recover liveness and effects                                                                                  │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule recover(env e) {
+    require nonpayable(e);
+
+    address receiver;
+    address other;
+
+    // sanity
+    requireInvariant noSelfWrap;
+    requireInvariant totalSupplyIsSumOfBalances;
+    requireInvariant totalSupplyIsSmallerThanUnderlyingBalance;
+
+    uint256 value                        = underlyingBalanceOf(currentContract) - totalSupply();
+    uint256 supplyBefore                 = totalSupply();
+    uint256 balanceBefore                = balanceOf(receiver);
+
+    uint256 otherBalanceBefore           = balanceOf(other);
+    uint256 otherUnderlyingBalanceBefore = underlyingBalanceOf(other);
+
+    recover@withrevert(e, receiver);
+    bool success = !lastReverted;
+
+    // liveness
+    assert success <=> receiver != 0;
+
+    // effect
+    assert success => (
+        balanceOf(receiver) == balanceBefore + value &&
+        totalSupply() == supplyBefore + value &&
+        totalSupply() == underlyingBalanceOf(currentContract)
+    );
+
+    // no side effect
+    assert underlyingBalanceOf(other) == otherUnderlyingBalanceBefore;
+    assert balanceOf(other) != otherBalanceBefore => other == receiver;
+}

contracts/token/ERC20/extensions/ERC20Wrapper.sol

@@ -19,6 +19,7 @@ abstract contract ERC20Wrapper is ERC20 {
     IERC20 private immutable _underlying;
 
     constructor(IERC20 underlyingToken) {
+        require(underlyingToken != this, "ERC20Wrapper: cannot self wrap");
         _underlying = underlyingToken;
     }
 
@@ -44,7 +45,9 @@ abstract contract ERC20Wrapper is ERC20 {
      * @dev Allow a user to deposit underlying tokens and mint the corresponding number of wrapped tokens.
      */
     function depositFor(address account, uint256 amount) public virtual returns (bool) {
-        SafeERC20.safeTransferFrom(_underlying, _msgSender(), address(this), amount);
+        address sender = _msgSender();
+        require(sender != address(this), "ERC20Wrapper: wrapper can't deposit");
+        SafeERC20.safeTransferFrom(_underlying, sender, address(this), amount);
         _mint(account, amount);
         return true;
     }