Certora Review #404

aave · May 24, 2024 · 2e59bf9 · 2e59bf9
1 parent 82f7ed2
commit 2e59bf9
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 4 deletions.
diff --git a/.github/workflows/certora-gsm.yml b/.github/workflows/certora-gsm.yml
@@ -58,7 +58,8 @@ jobs:
           - non-4626/Alex-gho-gsm.conf
           - non-4626/balances-buy.conf
           - non-4626/balances-sell.conf
-          - non-4626/Dominik-gho-assetToGhoInvertibility.conf --rule basicProperty_getAssetAmountForBuyAsset sellAssetInverse_all buyAssetInverse_all basicProperty_getGhoAmountForSellAsset basicProperty_getAssetAmountForSellAsset basicProperty_getGhoAmountForBuyAsset basicProperty2_getAssetAmountForBuyAsset
+          - non-4626/Dominik-gho-assetToGhoInvertibility.conf --rule basicProperty_getAssetAmountForBuyAsset sellAssetInverse_all buyAssetInverse_all basicProperty_getGhoAmountForSellAsset basicProperty_getAssetAmountForSellAsset basicProperty_getGhoAmountForBuyAsset
+          - non-4626/Dominik-gho-assetToGhoInvertibility.conf --rule basicProperty2_getAssetAmountForBuyAsset
           - non-4626/Dominik-gho-fixedPriceStrategy.conf
           - non-4626/fees-buy.conf
           - non-4626/fees-sell.conf

diff --git a/certora/GSM/specs/gsm/Dominik-AssetToGhoInvertibility.spec b/certora/GSM/specs/gsm/Dominik-AssetToGhoInvertibility.spec
@@ -18,7 +18,7 @@ function mulDivSummary(uint256 x, uint256 y, uint256 denominator) returns uint25
 function mulDivSummaryWithRounding(uint256 x, uint256 y, uint256 denominator, Math.Rounding rounding) returns uint256
 {
     require denominator > 0;
-    if rounding == Math.Rounding.Up
+    if (rounding == Math.Rounding.Up)
     {
         return require_uint256((x * y + denominator - 1) / denominator);
     }
@@ -297,4 +297,4 @@ rule sellAssetInverse_all() {
     assert grossAmount2 <= grossAmount && to_mathint(grossAmount) <= grossAmount2 + 1, "gross amount off by at most 1";
     assert fee2 <= fee && to_mathint(fee) <= fee2 + 1, "fee by at most 1";
     assert (fee == fee2) <=> (grossAmount == grossAmount2), "fee off by 1 iff gross amount off by 1";
-}
+}
diff --git a/certora/GSM/specs/gsm/Dominik-FixedPriceStrategy.spec b/certora/GSM/specs/gsm/Dominik-FixedPriceStrategy.spec
@@ -19,7 +19,7 @@ function mulDivSummary(uint256 x, uint256 y, uint256 denominator) returns uint25
 function mulDivSummaryWithRounding(uint256 x, uint256 y, uint256 denominator, Math.Rounding rounding) returns uint256
 {
     require denominator > 0;
-    if rounding == Math.Rounding.Up
+    if (rounding == Math.Rounding.Up)
     {
         return require_uint256((x * y + denominator - 1) / denominator);
     }