Finish ERC20Wrapper

certora/harnesses/ERC20WrapperHarness.sol

@@ -2,10 +2,15 @@
 
 pragma solidity ^0.8.20;
 
-import "../patched/token/ERC20/extensions/ERC20Wrapper.sol";
+import {ERC20Permit} from "../patched/token/ERC20/extensions/ERC20Permit.sol";
+import {ERC20Wrapper, IERC20, ERC20} from "../patched/token/ERC20/extensions/ERC20Wrapper.sol";
 
-contract ERC20WrapperHarness is ERC20Wrapper {
-    constructor(IERC20 _underlying, string memory _name, string memory _symbol) ERC20(_name, _symbol) ERC20Wrapper(_underlying) {}
+contract ERC20WrapperHarness is ERC20Permit, ERC20Wrapper {
+    constructor(
+        IERC20 _underlying,
+        string memory _name,
+        string memory _symbol
+    ) ERC20(_name, _symbol) ERC20Permit(_name) ERC20Wrapper(_underlying) {}
 
     function underlyingTotalSupply() public view returns (uint256) {
         return underlying().totalSupply();
@@ -22,4 +27,8 @@ contract ERC20WrapperHarness is ERC20Wrapper {
     function recover(address account) public returns (uint256) {
         return _recover(account);
     }
+
+    function decimals() public view override(ERC20Wrapper, ERC20) returns (uint8) {
+        return super.decimals();
+    }
 }

certora/specs/ERC20Wrapper.spec

@@ -1,18 +1,18 @@
-import "helpers/helpers.spec"
-import "ERC20.spec"
+import "helpers/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)
+    function underlying()                       external returns(address) envfree;
+    function underlyingTotalSupply()            external returns(uint256) envfree;
+    function underlyingBalanceOf(address)       external returns(uint256) envfree;
+    function underlyingAllowanceToThis(address) external returns(uint256) envfree;
+
+    function depositFor(address, uint256)       external returns(bool);
+    function withdrawTo(address, uint256)       external returns(bool);
+    function recover(address)                   external returns(uint256);
 }
 
-use invariant totalSupplyIsSumOfBalances
+use invariant totalSupplyIsSumOfBalances;
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@@ -24,7 +24,7 @@ function underlyingBalancesLowerThanUnderlyingSupply(address a) returns bool {
 }
 
 function sumOfUnderlyingBalancesLowerThanUnderlyingSupply(address a, address b) returns bool {
-    return a != b => underlyingBalanceOf(a) + underlyingBalanceOf(b) <= underlyingTotalSupply();
+    return a != b => underlyingBalanceOf(a) + underlyingBalanceOf(b) <= to_mathint(underlyingTotalSupply());
 }
 
 /*
@@ -47,7 +47,7 @@ invariant totalSupplyIsSmallerThanUnderlyingBalance()
     }
 
 invariant noSelfWrap()
-    currentContract != underlying()
+    currentContract != underlying();
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@@ -85,6 +85,7 @@ rule depositFor(env e) {
     assert success <=> (
         sender   != currentContract               && // invalid sender
         sender   != 0                             && // invalid sender
+        receiver != currentContract               && // invalid receiver
         receiver != 0                             && // invalid receiver
         amount   <= senderUnderlyingBalanceBefore && // deposit doesn't exceed balance
         amount   <= senderUnderlyingAllowanceBefore  // deposit doesn't exceed allowance
@@ -92,10 +93,10 @@ rule depositFor(env e) {
 
     // effects
     assert success => (
-        balanceOf(receiver) == balanceBefore + amount &&
-        totalSupply() == supplyBefore + amount &&
-        underlyingBalanceOf(currentContract) == wrapperUnderlyingBalanceBefore + amount &&
-        underlyingBalanceOf(sender) == senderUnderlyingBalanceBefore - amount
+        to_mathint(balanceOf(receiver)) == balanceBefore + amount &&
+        to_mathint(totalSupply()) == supplyBefore + amount &&
+        to_mathint(underlyingBalanceOf(currentContract)) == wrapperUnderlyingBalanceBefore + amount &&
+        to_mathint(underlyingBalanceOf(sender)) == senderUnderlyingBalanceBefore - amount
     );
 
     // no side effect
@@ -137,17 +138,18 @@ rule withdrawTo(env e) {
 
     // liveness
     assert success <=> (
-        sender   != 0          && // invalid sender
-        receiver != 0          && // invalid receiver
-        amount   <= balanceBefore // withdraw doesn't exceed balance
+        sender   != 0               && // invalid sender
+        receiver != currentContract && // invalid receiver
+        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)
+        to_mathint(balanceOf(sender)) == balanceBefore - amount &&
+        to_mathint(totalSupply()) == supplyBefore - amount &&
+        to_mathint(underlyingBalanceOf(currentContract)) == wrapperUnderlyingBalanceBefore - (currentContract != receiver ? amount : 0) &&
+        to_mathint(underlyingBalanceOf(receiver)) == receiverUnderlyingBalanceBefore + (currentContract != receiver ? amount : 0)
     );
 
     // no side effect
@@ -172,7 +174,7 @@ rule recover(env e) {
     requireInvariant totalSupplyIsSumOfBalances;
     requireInvariant totalSupplyIsSmallerThanUnderlyingBalance;
 
-    uint256 value                        = underlyingBalanceOf(currentContract) - totalSupply();
+    mathint value                        = underlyingBalanceOf(currentContract) - totalSupply();
     uint256 supplyBefore                 = totalSupply();
     uint256 balanceBefore                = balanceOf(receiver);
 
@@ -187,8 +189,8 @@ rule recover(env e) {
 
     // effect
     assert success => (
-        balanceOf(receiver) == balanceBefore + value &&
-        totalSupply() == supplyBefore + value &&
+        to_mathint(balanceOf(receiver)) == balanceBefore + value &&
+        to_mathint(totalSupply()) == supplyBefore + value &&
         totalSupply() == underlyingBalanceOf(currentContract)
     );