Merge branch 'certora/erc20' of github.com:Certora/openzeppelin-contracts into remotes/origin/certora/erc20

certora/specs/ERC20FlashMint.spec

@@ -1,7 +1,7 @@
 import "erc20.spec"
 
 methods {
-    onFlashLoan(address, address, uint256, uint256, bytes) => HAVOC_ALL // HAVOC_ECF
+    onFlashLoan(address, address, uint256, uint256, bytes) => HAVOC_ALL
 
     _burn(address account, uint256 amount) returns(bool) => specBurn(account, amount);
 }
@@ -13,19 +13,11 @@ function specBurn(address account, uint256 amount) returns bool {   // retuns ne
     return true;
 }
 
-// ghost to save args that were passed to burn function
-// summarize burn
-// assert ghost == amount + fee
 
-
-// STATUS - in progress
-// HAVOC_ALL - everything is havoced => violation
-// HAVOC_ECF - verified
-// https://vaas-stg.certora.com/output/3106/8795450b626f2ca53a2b/?anonymousKey=dd774da10cc595e4e38357af9e4f50bf2c0cb02a
+// STATUS - verified
 // fee + flashLoan amount is burned
 rule letsWatchItBurns(env e){
     address receiver; address token; uint256 amount; bytes data;
-    require amount > 0;
 
     uint256 feeBefore = flashFee(e, token, amount);
 

certora/specs/ERC20Wrapper.spec

@@ -12,7 +12,7 @@ methods {
 
 
 // STATUS - verified
-// totalsupply of wrapped should be less than or equal to underlying (assuming no transfer they should be equal) - solvency
+// totalsupply of wrapped should be less than or equal to underlying (assuming no external transfer) - solvency
 invariant whatAboutTotal(env e)
     totalSupply(e) <= underlyingTotalSupply()
     filtered { f -> f.selector != certorafallback_0().selector }
@@ -29,6 +29,18 @@ invariant whatAboutTotal(env e)
     }
 
 
+// STATUS - in progress
+// https://vaas-stg.certora.com/output/3106/a5f4943cd2987dccab94/?anonymousKey=9428fb1588845c0222c2abe5b00dedd59c925870
+// totalsupply of wrapped should be less than or equal to the underlying balanceOf contract (assuming no external transfer) - solvency
+invariant underTotalAndContractBalanceOfCorrelation(env e)
+    totalSupply(e) <= underlyingBalanceOf(currentContract)
+    {
+        preserved {
+            require underlying() != currentContract;
+        }
+    }
+
+
 // STATUS - verified
 // check correct values update by depositFor()
 rule depositForSpecBasic(env e){