Add FV specification for ERC20Wrapper

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

@@ -24,7 +24,7 @@ const [reqSpec, reqContract] = request.split(':').reverse();
 
 for (const { spec, contract, files, options = [] } of Object.values(specs)) {
   if ((!reqSpec || reqSpec === spec) && (!reqContract || reqContract === contract)) {
-    limit(runCertora, spec, contract, files, [...options, ...extraOptions]);
+    limit(runCertora, spec, contract, files, [...options.flatMap(opt => opt.split(' ')), ...extraOptions]);
   }
 }
 
@@ -44,7 +44,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;
       }
@@ -64,7 +64,7 @@ async function runCertora(spec, contract, files, options = []) {
   stream.end();
 
   // write results in markdown format
-  writeEntry(spec, contract, code || signal, (await output).match(/https:\S*/)[0]);
+  writeEntry(spec, contract, code || signal, (await output).match(/https:\S*/)?.[0]);
 
   // write all details
   console.error(`+ certoraRun ${args.join(' ')}\n` + (await output));
@@ -102,8 +102,8 @@ function writeEntry(spec, contract, success, url) {
       spec,
       contract,
       success ? ':x:' : ':heavy_check_mark:',
-      `[link](${url})`,
-      `[link](${url.replace('/jobStatus/', '/output/')})`,
+      url ? `[link](${url})` : 'error',
+      url ? `[link](${url?.replace('/jobStatus/', '/output/')})` : 'error',
     ),
   );
 }

certora/specs.json

@@ -18,5 +18,17 @@
       "certora/harnesses/ERC3156FlashBorrowerHarness.sol"
     ],
     "options": ["--optimistic_loop"]
+  },
+  {
+    "spec": "ERC20Wrapper",
+    "contract": "ERC20WrapperHarness",
+    "files": [
+      "certora/harnesses/ERC20PermitHarness.sol",
+      "certora/harnesses/ERC20WrapperHarness.sol"
+    ],
+    "options": [
+      "--link ERC20WrapperHarness:_underlying=ERC20PermitHarness",
+      "--optimistic_loop"
+    ]
   }
 ]

certora/specs/ERC20Wrapper.spec

@@ -0,0 +1,190 @@
+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 sumOfUnderlyingBalancesLowerThanUnderlyingSupply(address a, address b) {
+    if (a != b) {
+        require underlyingBalanceOf(a) + underlyingBalanceOf(b) <= underlyingTotalSupply();
+    } else {
+        require underlyingBalanceOf(a) <= 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 underlyingBalanceOf(currentContract) <= underlyingTotalSupply();
+        }
+        preserved depositFor(address account, uint256 amount) with (env e) {
+            require e.msg.sender != currentContract;
+            sumOfUnderlyingBalancesLowerThanUnderlyingSupply(e.msg.sender, currentContract);
+        }
+    }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: depositFor liveness and effects                                                                               │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule depositFor(env e) {
+    require nonpayable(e);
+
+    address sender = e.msg.sender;
+    address receiver;
+    address other;
+    uint256 amount;
+
+    // sanity
+    require currentContract != sender;
+    require currentContract != underlying();
+    requireInvariant totalSupplyIsSumOfBalances;
+    requireInvariant totalSupplyIsSmallerThanUnderlyingBalance;
+    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   != 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;
+    assert success => totalSupply()                        == supplyBefore                   + amount;
+    assert success => underlyingBalanceOf(currentContract) == wrapperUnderlyingBalanceBefore + amount;
+    assert success => 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
+    require currentContract != underlying();
+    requireInvariant totalSupplyIsSumOfBalances;
+    requireInvariant totalSupplyIsSmallerThanUnderlyingBalance;
+    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;
+    assert success => totalSupply()                        == supplyBefore                    - amount;
+    assert success => underlyingBalanceOf(currentContract) == wrapperUnderlyingBalanceBefore  - (currentContract != receiver ? amount : 0);
+    assert success => 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
+    require currentContract != underlying();
+    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;
+    assert success => totalSupply()       == supplyBefore  + value;
+    assert success => totalSupply()       == underlyingBalanceOf(currentContract);
+
+    // no side effect
+    assert underlyingBalanceOf(other) == otherUnderlyingBalanceBefore;
+    assert balanceOf(other) != otherBalanceBefore => other == receiver;
+}