reverting to old syntax

Certora · Jan 12, 2025 · e25ab8a · e25ab8a
1 parent 5050fe5
commit e25ab8a
Show file tree

Hide file tree

Showing 5 changed files with 6 additions and 5 deletions.
diff --git a/.github/workflows/certora-GSM-4626.yml b/.github/workflows/certora-GSM-4626.yml
@@ -63,6 +63,7 @@ jobs:
           - getAmount_4626_properties.conf --rule getGhoAmountForBuyAsset_correctness
           - getAmount_4626_properties.conf --rule getGhoAmountForSellAsset_optimality getAssetAmountForSellAsset_optimality getAssetAmountForBuyAsset_funcProperty
           - finishedRules4626.conf --rule cantBuyOrSellWhenSeized cantBuyOrSellWhenFrozen sellAssetIncreasesExposure buyAssetDecreasesExposure rescuingAssetKeepsAccruedFees rescuingGhoKeepsAccruedFees giftingGhoDoesntAffectStorageSIMPLE correctnessOfBuyAsset giftingUnderlyingDoesntAffectStorageSIMPLE sellAssetSameAsGetGhoAmountForSellAsset correctnessOfSellAsset giftingGhoDoesntCreateExcessOrDearth backWithGhoDoesntCreateExcess getAssetAmountForSellAsset_correctness collectedSellFeeIsAtLeastAsRequired collectedBuyFeePlus2IsAtLeastAsRequired collectedBuyFeePlus1IsAtLeastAsRequired collectedBuyFeeIsAtLeastAsRequired sellingDoesntExceedExposureCap whoCanChangeAccruedFees whoCanChangeExposure
+          - finishedRules4626.conf --rule giftingUnderlyingDoesntCreateExcessOrDearth
 
 
 

diff --git a/.github/workflows/certora-gsm.yml b/.github/workflows/certora-gsm.yml
@@ -48,7 +48,7 @@ jobs:
       max-parallel: 16
       matrix:
         rule:
-          - gho-gsm_inverse.conf
+          - gho-gsm_inverse.confxr
           - gho-gsm.conf
           - balances-buy.conf
           - balances-sell.conf

diff --git a/certora/gho/specs/VariableDebtToken.spec b/certora/gho/specs/VariableDebtToken.spec
@@ -34,12 +34,12 @@ ghost sumAllBalance() returns mathint {
     init_state axiom sumAllBalance() == 0;
 }
 
-hook Sstore _userState[KEY address a].balance uint128 balance (uint128 old_balance) {
+hook Sstore _userState[KEY address a].balance uint128 balance (uint128 old_balance) STORAGE {
   havoc sumAllBalance assuming sumAllBalance@new() == sumAllBalance@old() + balance - old_balance;
 }
 
 invariant totalSupplyEqualsSumAllBalance(env e)
-    totalSupply() == scaledBalanceOfToBalanceOf(require_uint256(sumAllBalance()))
+    totalSupply() == scaledBalanceOfToBalanceOf(sumAllBalance())
     filtered { f -> !f.isView && !disAllowedFunctions(f) }
     {
         preserved mint(address user, address onBehalfOf, uint256 amount, uint256 index) with (env e2) {

diff --git a/certora/gho/specs/summarizations.spec b/certora/gho/specs/summarizations.spec
@@ -4,7 +4,7 @@ function first_term(uint256 x, uint256 y) returns uint256 { return x; }
 ghost mapping(uint256 => mapping(uint256 => uint256)) rayMulSummariztionValues;
 function rayMulSummariztion(uint256 x, uint256 y) returns uint256
 {
-	if (x == 0 || y == 0)
+	if ((x == 0) || (y == 0))
 	{
 		return 0;
 	}

diff --git a/certora/gsm/specs/gsm/gho-gsm-finishedRules.spec b/certora/gsm/specs/gsm/gho-gsm-finishedRules.spec
@@ -316,7 +316,7 @@ rule getAssetAmountForSellAsset_optimality()
 // @title Exposure below cap is preserved by all methods except updateExposureCap and initialize
 // STATUS: PASS
 // https://prover.certora.com/output/6893/14a1440d3114460f8b64b388a706ca46/?anonymousKey=bb420c63b5b5b11810d5d72026ed6cb6baec43ac
-rule exposureBellowCap(method f)
+rule exposureBelowCap(method f)
 	filtered { f -> 
 		f.selector != sig:initialize(address,address,uint128).selector
 		&& f.selector != sig:updateExposureCap(uint128).selector