From 2e59bf99892ec248e5308550ae43d78e849e902d Mon Sep 17 00:00:00 2001
From: Nissan Levi <124057587+nisnislevi@users.noreply.github.com>
Date: Fri, 24 May 2024 09:50:53 +0300
Subject: [PATCH] Certora Review #404

---
 .github/workflows/certora-gsm.yml                          | 3 ++-
 certora/GSM/specs/gsm/Dominik-AssetToGhoInvertibility.spec | 4 ++--
 certora/GSM/specs/gsm/Dominik-FixedPriceStrategy.spec      | 2 +-
 3 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/certora-gsm.yml b/.github/workflows/certora-gsm.yml
index 9ab38e9d..85f061e4 100644
--- 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
index 8d0eb733..65b639de 100644
--- 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";
-}
\ No newline at end of file
+}
diff --git a/certora/GSM/specs/gsm/Dominik-FixedPriceStrategy.spec b/certora/GSM/specs/gsm/Dominik-FixedPriceStrategy.spec
index 572c9b50..fa55cca3 100644
--- 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);
     }