From 8318470ccaf7d5343683a915f6d516ecf8451367 Mon Sep 17 00:00:00 2001
From: Aleksander Kryukov <firealexkryukov@gmail.com>
Date: Wed, 23 Mar 2022 19:12:16 +0000
Subject: [PATCH 1/2] flashMint cleaning

---
 certora/specs/ERC20FlashMint.spec | 12 ++----------
 1 file changed, 2 insertions(+), 10 deletions(-)

diff --git a/certora/specs/ERC20FlashMint.spec b/certora/specs/ERC20FlashMint.spec
index db8cddcad..511eaf84f 100644
--- a/certora/specs/ERC20FlashMint.spec
+++ b/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);
 

From 5153c462d50890d82cb3dc11b0c0272a5c6cf639 Mon Sep 17 00:00:00 2001
From: Aleksander Kryukov <firealexkryukov@gmail.com>
Date: Wed, 23 Mar 2022 19:42:14 +0000
Subject: [PATCH 2/2] wrapper counterexample to check

---
 certora/specs/ERC20Wrapper.spec | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

diff --git a/certora/specs/ERC20Wrapper.spec b/certora/specs/ERC20Wrapper.spec
index 6e40c61d2..126be7297 100644
--- a/certora/specs/ERC20Wrapper.spec
+++ b/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){