test: separate confs

Layr-Labs · May 24, 2024 · 6c5d1ab · 6c5d1ab
1 parent 6cc81c4
commit 6c5d1ab
Show file tree

Hide file tree

Showing 3 changed files with 29 additions and 11 deletions.
diff --git a/certora/config/paymentCoordinator.conf b/certora/config/paymentCoordinator.conf
@@ -16,11 +16,12 @@
     "optimistic_loop": true,
     "optimistic_hashing": true,
     "rule_sanity": "basic",
+    "exclude_rule": ["checkClaimNeverFalse"],
     "mutations": {
         "gambit": [
             {
                 "filename" : "src/contracts/core/PaymentCoordinator.sol",
-                "num_mutants": 5
+                "num_mutants": 20
             }
         ],
     }

diff --git a/certora/config/paymentCoordinatorWithoutSanity.conf b/certora/config/paymentCoordinatorWithoutSanity.conf
@@ -0,0 +1,26 @@
+{
+    "files": [
+        "lib/openzeppelin-contracts/contracts/token/ERC20/ERC20.sol",
+        "lib/openzeppelin-contracts/contracts/token/ERC20/presets/ERC20PresetFixedSupply.sol",
+        "certora/harnesses/PaymentCoordinatorHarness.sol"
+    ],
+    "verify": "PaymentCoordinatorHarness:certora/specs/core/PaymentCoordinator.spec",
+    "loop_iter": "2",
+    "parametric_contracts": ["PaymentCoordinatorHarness"],
+    "packages": [
+        "@openzeppelin=lib/openzeppelin-contracts",
+        "@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable"
+    ],
+    "link": [],
+    "optimistic_fallback": true,
+    "optimistic_loop": true,
+    "optimistic_hashing": true,
+    "mutations": {
+        "gambit": [
+            {
+                "filename" : "src/contracts/core/PaymentCoordinator.sol",
+                "num_mutants": 20
+            }
+        ],
+    }
+}
diff --git a/certora/specs/core/PaymentCoordinator.spec b/certora/specs/core/PaymentCoordinator.spec
@@ -3,12 +3,6 @@ using ERC20 as token1;
 using ERC20PresetFixedSupply as token2;
 
 methods {
-
-
-    // function MerkleTree.getValue(address, address) external returns(uint256) envfree;
-    // function MerkleTree.getHash(bytes32) external returns(bytes32) envfree;
-    // function MerkleTree.wellFormedPath(bytes32, bytes32[]) external envfree;
-
     function _.balanceOf(address) external => DISPATCHER(true);
     function _.transfer(address, uint256) external => DISPATCHER(true);
     function _.transferFrom(address, address, uint256) external => DISPATCHER(true);
@@ -40,9 +34,6 @@ rule claimWithduplicateTokenLeafs(env e, IPaymentCoordinator.PaymentMerkleClaim
     require claim.tokenLeaves.length == 1;
 
     checkClaim(e, claim);
-    // bool canWork = claimerFor(e, claim.earnerLeaf.earner) != 0 ? 
-    //     e.msg.sender == claimerFor(e, claim.earnerLeaf.earner) :
-    //     e.msg.sender == claim.earnerLeaf.earner;
 
     if ((claimerFor(e, claim.earnerLeaf.earner)) != 0) {
         require e.msg.sender == claimerFor(e, claim.earnerLeaf.earner);
@@ -59,7 +50,7 @@ rule claimWithduplicateTokenLeafs(env e, IPaymentCoordinator.PaymentMerkleClaim
     );
 }
 
-/// status: pending
+/// status: pass
 rule cumulativeClaimedStrictlyIncreasing(env e, address claimToken, address earner) {
     uint256 cumulativeClaimedBefore = cumulativeClaimed(earner, claimToken);
     calldataarg args;