cleanup certora specs

0xb337r007 · Jul 22, 2024 · 796acc7 · 796acc7
1 parent c16f67e
commit 796acc7
Show file tree

Hide file tree

Showing 5 changed files with 1 addition and 55 deletions.
diff --git a/certora/confs/Marketplace.conf b/certora/confs/Marketplace.conf
@@ -2,7 +2,6 @@
     "files": [
         "contracts/Marketplace.sol",
         "contracts/Groth16Verifier.sol",
-        //"certora/harness/MarketplaceHarness.sol",
         "certora/helpers/ERC20A.sol",
     ],
     "parametric_contracts": ["Marketplace"],
@@ -15,7 +14,6 @@
     "verify": "Marketplace:certora/specs/Marketplace.spec",
     "optimistic_loop": true,
     "loop_iter": "3",
-    "solc": "solc8.23",
     "optimistic_hashing": true,
     "hashing_length_bound": "512",
 }

diff --git a/certora/harness/MarketplaceHarness.sol b/certora/harness/MarketplaceHarness.sol
diff --git a/certora/helpers/ERC20B.sol b/certora/helpers/ERC20B.sol
diff --git a/certora/specs/Marketplace.spec b/certora/specs/Marketplace.spec
@@ -1,10 +1,5 @@
 using ERC20A as Token;
 
-methods {
-
-}
-
-
 /*--------------------------------------------
 |              Ghosts and hooks              |
 --------------------------------------------*/
@@ -29,8 +24,6 @@ hook Sstore currentContract._marketplaceTotals.sent uint256 defaultValue (uint25
     totalSent = totalSent + defaultValue - defaultValue_old;
 }
 
-
-
 /*--------------------------------------------
 |                 Properties                 |
 --------------------------------------------*/
@@ -63,14 +56,3 @@ rule totalSentCannotDecrease(env e, method f) {
 
     assert total_after >= total_before;
 }
-
-rule whatCanChangeCOntractTOkenBalance(env e, method f) {
-    uint256 tokenBalanceBefore = Token.balanceOf(e, currentContract);
-
-    calldataarg args;
-    f(e, args);
-
-    uint256 tokenBalanceAfter = Token.balanceOf(e, currentContract);
-
-    assert tokenBalanceBefore == tokenBalanceAfter;
-}
diff --git a/package.json b/package.json
@@ -10,7 +10,7 @@
     "format:check": "prettier --check contracts/**/*.sol test/**/*.js",
     "lint": "solhint contracts/**.sol",
     "deploy": "hardhat deploy",
-    "verify": "pnpm verify:marketplace && pnpm verify:marketplace",
+    "verify": "pnpm verify:marketplace",
     "verify:marketplace": "certoraRun certora/confs/Marketplace.conf"
   },
   "devDependencies": {