feat: check increasing claim amounts

morpho-org · Mar 11, 2024 · b6f4f2a · b6f4f2a
1 parent f5daa10
commit b6f4f2a
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/certora/specs/RewardsDistributor.spec b/certora/specs/RewardsDistributor.spec
@@ -39,11 +39,12 @@ rule claimTwice(address _account, uint256 _claim1, uint256 _claim2) {
     bytes32[] _proof1; bytes32[] _proof2;
     claim(_account, _claim1, _proof1);
     claim(_account, _claim2, _proof2);
+    assert _claim2 >= _claim1;
 
     storage afterBothStorage = lastStorage;
 
-    bytes32[] _proof;
-    claim(_account, _claim2, _proof) at initStorage;
+    bytes32[] _proof3;
+    claim(_account, _claim2, _proof3) at initStorage;
 
     assert lastStorage == afterBothStorage;
 }