fix: certora prover changes

aave · Oct 18, 2023 · 2aa874c · 2aa874c
1 parent 4c54320
commit 2aa874c
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 39 deletions.
diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
@@ -34,7 +34,7 @@ jobs:
         with: { java-version: '11', java-package: jre }
 
       - name: Install certora cli
-        run: pip install certora-cli==3.6.8.post3
+        run: pip install certora-cli
 
       - name: Install solc
         run: |

diff --git a/certora/scripts/verifyGhoToken.sh b/certora/scripts/verifyGhoToken.sh
@@ -8,7 +8,7 @@ certoraRun certora/harness/GhoTokenHarness.sol:GhoTokenHarness certora/munged/co
     --loop_iter 3 \
     --optimistic_loop \
     --rules "${@}" \
-    --msg "GhoToken, rules ${@}"
+    --msg "GhoToken workaround for CERT-1060, rules ${@}"
 else
 certoraRun certora/harness/GhoTokenHarness.sol:GhoTokenHarness certora/munged/contracts/gho/GhoToken.sol \
     --verify GhoTokenHarness:certora/specs/ghoToken.spec \

diff --git a/certora/specs/ghoToken.spec b/certora/specs/ghoToken.spec
@@ -214,8 +214,6 @@ rule mint_after_burn(method f) filtered {f -> !f.isView}
 	requireInvariant inv_balanceOf_leq_totalSupply(e.msg.sender);
 	requireInvariant inv_valid_capacity(e.msg.sender);
 
-	require amount_mint > 0;
-
 	burn(e, amount_burn);
 	f(e, arg);
 	mint@withrevert(e, account, amount_mint);
@@ -525,39 +523,7 @@ rule address_not_in_list_after_removeFacilitator_CASE_SPLIT_zero_address(address
 	assert !is_in_facilitator_set_array(facilitator);
 }
 
-// if facilitator exist it has to remain exist unless facilitator manager calls an action
-// if facilitator not exist it has to remain not exist unless facilitator manager calls an action
-rule OnlyFacilitatorManagerAlterFacilitatorExistence(){
-    env e;
-    address facilitator;
-    bool _facilitatorExist = is_in_facilitator_mapping(facilitator);
-    bool isSenderManager = hasRole(FACILITATOR_MANAGER(), e.msg.sender);
-
-    method f; calldataarg args;
-    f(e, args);
-
-    bool facilitatorExist_ = is_in_facilitator_mapping(facilitator);
-
-    assert (_facilitatorExist && !isSenderManager) => facilitatorExist_;
-    assert (!_facilitatorExist && !isSenderManager) => !facilitatorExist_;
-}
 
-// facilitator exist && msg.sender != checkrole(bucketManager) => getBucketCapacity_ == _getBucketCapacity
-rule OnlyBucketManagerCanChangeCapacity(){
-    env e;
-    address facilitator;
-    bool _facilitatorExist = is_in_facilitator_mapping(facilitator);
-    uint256 _bucketCapacity = getFacilitatorBucketCapacity(facilitator);
-    bool isSenderBucketManager = hasRole(BUCKET_MANAGER(), e.msg.sender);
-    bool isSenderFacilitatorManager = hasRole(FACILITATOR_MANAGER(), e.msg.sender);
-
-
-    method f; calldataarg args;
-    f(e, args);
-
-    uint256 bucketCapacity_ = getFacilitatorBucketCapacity(facilitator);
-
-    assert (_facilitatorExist && !isSenderBucketManager) => 
-                    ((bucketCapacity_ == _bucketCapacity) || 
-                        (isSenderFacilitatorManager && bucketCapacity_ == 0));
-}
+
+
+