From f037c2a4d75f54b4136805b790f8de84da66df02 Mon Sep 17 00:00:00 2001
From: Devashish Tomar <soham.tomar@yahoo.com>
Date: Sat, 21 Oct 2023 14:37:13 +0400
Subject: [PATCH] Added Gambit configs and improved PolygonMigration.spec file

---
 .gitignore                                    |  5 +++-
 .../confs/gambit/defaultEmissionManger.conf   |  8 ++++++
 .../confs/gambit/polygonEcosystemToken.conf   |  7 +++++
 certora/confs/gambit/polygonMigration.conf    |  8 ++++++
 certora/specs/PolygonMigration.spec           | 27 +++++++++++++++++++
 5 files changed, 54 insertions(+), 1 deletion(-)
 create mode 100644 certora/confs/gambit/defaultEmissionManger.conf
 create mode 100644 certora/confs/gambit/polygonEcosystemToken.conf
 create mode 100644 certora/confs/gambit/polygonMigration.conf

diff --git a/.gitignore b/.gitignore
index c0f97fc..7f8014f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -11,4 +11,7 @@ broadcast/*/31337
 deployments/31337.md
 deployments/json/31337.json
 
-.certora_internal
\ No newline at end of file
+# Certora and Gambit cache
+.certora_internal
+collect.json
+collection_failures.txt
\ No newline at end of file
diff --git a/certora/confs/gambit/defaultEmissionManger.conf b/certora/confs/gambit/defaultEmissionManger.conf
new file mode 100644
index 0000000..9ffa579
--- /dev/null
+++ b/certora/confs/gambit/defaultEmissionManger.conf
@@ -0,0 +1,8 @@
+{
+  "filename": "../../../src/DefaultEmissionManager.sol",
+  "solc_remappings": [
+    "openzeppelin-contracts=../../../lib/openzeppelin-contracts/",
+    "openzeppelin-contracts-upgradeable=../../../lib/openzeppelin-contracts-upgradeable/"
+  ],
+  "num_mutants" : 30
+}
\ No newline at end of file
diff --git a/certora/confs/gambit/polygonEcosystemToken.conf b/certora/confs/gambit/polygonEcosystemToken.conf
new file mode 100644
index 0000000..e486f5e
--- /dev/null
+++ b/certora/confs/gambit/polygonEcosystemToken.conf
@@ -0,0 +1,7 @@
+{
+  "filename": "../../../src/PolygonEcosystemToken.sol",
+  "solc_remappings": [
+    "openzeppelin-contracts=../../../lib/openzeppelin-contracts/"
+  ],
+  "num_mutants" : 30
+}
\ No newline at end of file
diff --git a/certora/confs/gambit/polygonMigration.conf b/certora/confs/gambit/polygonMigration.conf
new file mode 100644
index 0000000..17f1ff3
--- /dev/null
+++ b/certora/confs/gambit/polygonMigration.conf
@@ -0,0 +1,8 @@
+{
+  "filename": "../../../src/PolygonMigration.sol",
+  "solc_remappings": [
+    "openzeppelin-contracts=../../../lib/openzeppelin-contracts/",
+    "openzeppelin-contracts-upgradeable=../../../lib/openzeppelin-contracts-upgradeable/"
+  ],
+  "num_mutants" : 30
+}
\ No newline at end of file
diff --git a/certora/specs/PolygonMigration.spec b/certora/specs/PolygonMigration.spec
index 7788519..216ed49 100644
--- a/certora/specs/PolygonMigration.spec
+++ b/certora/specs/PolygonMigration.spec
@@ -226,6 +226,12 @@ rule unmigrateWithPermit(env e) {
             => assert_uint256(0) == callerAllowanceAfter;
 
         assert to_mathint(_PolygonEcosystemToken.nonces(holder)) == nonceBefore + 1;
+        
+        assert require_uint256(polygonBalanceBeforeCaller - amount) == polygonBalanceAfterCaller && 
+            require_uint256(maticBalanceBeforeCaller + amount) == maticBalanceAfterCaller;
+
+        assert require_uint256(polygonBalanceBeforeContract + amount) == polygonBalanceAfterContract && 
+            require_uint256(maticBalanceBeforeContract - amount) == maticBalanceAfterContract;
 
         // deadline was respected
         assert deadline >= e.block.timestamp;
@@ -278,4 +284,25 @@ rule verifyMigrate(env e) {
         assert assert_uint256(maticBalanceBeforeContract + amount) == maticBalanceAfterContract;
         assert polygonBalanceBeforeOther == polygonBalanceAfterOther && polygonBalanceAfterOther == polygonBalanceAfterOther;
     }
+}
+
+rule shouldRevertIfUnmigrateIsLocked(env e) {
+
+    uint256 amount;
+
+    requireInvariant totalSupplyIsSumOfBalances();
+    require nonpayable(e);
+    require nonzerosender(e);
+    require e.msg.sender != currentContract;
+    require (_PolygonEcosystemToken.allowance(e.msg.sender, currentContract)) >= amount;
+
+    require (_PolygonEcosystemToken.balanceOf(e.msg.sender) >= amount);
+    require (_Matic.balanceOf(currentContract) >= amount);
+        
+    unmigrate@withrevert(e, amount);
+
+    bool didUnmigrateRevert = lastReverted;
+
+    assert didUnmigrateRevert => unmigrationLocked() == true;
+
 }
\ No newline at end of file