From f95b266f18fc42766b50a3ddf6f7121388689266 Mon Sep 17 00:00:00 2001 From: Michael M Date: Thu, 25 Jan 2024 14:08:55 +0200 Subject: [PATCH] adapting to changes in exposure type --- certora/GSM/harness/GsmHarness.sol | 2 +- .../GSM/specs/gsm/otakar-gho-gsm-finishedRules.spec | 12 ++++++------ 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/certora/GSM/harness/GsmHarness.sol b/certora/GSM/harness/GsmHarness.sol index f1fc4df3..b336ed5b 100644 --- a/certora/GSM/harness/GsmHarness.sol +++ b/certora/GSM/harness/GsmHarness.sol @@ -19,7 +19,7 @@ contract GsmHarness is Gsm { return _accruedFees; } - function getCurrentExposure() external view returns (uint256) { + function getCurrentExposure() external view returns (uint128) { return _currentExposure; } diff --git a/certora/GSM/specs/gsm/otakar-gho-gsm-finishedRules.spec b/certora/GSM/specs/gsm/otakar-gho-gsm-finishedRules.spec index 2ba88f65..8f3524b1 100644 --- a/certora/GSM/specs/gsm/otakar-gho-gsm-finishedRules.spec +++ b/certora/GSM/specs/gsm/otakar-gho-gsm-finishedRules.spec @@ -56,7 +56,7 @@ rule buyAssetDecreasesExposure() priceLimits(e); uint128 amount; address receiver; - uint exposureBefore = getCurrentExposure(e); + uint128 exposureBefore = getCurrentExposure(e); require amount > 0; buyAsset(e, amount, receiver); @@ -74,7 +74,7 @@ rule sellAssetIncreasesExposure() priceLimits(e); uint128 amount; address receiver; - uint exposureBefore = getCurrentExposure(e); + uint128 exposureBefore = getCurrentExposure(e); require amount > 0; sellAsset(e, amount, receiver); @@ -93,8 +93,8 @@ rule cantSellIfExposureTooHigh() address receiver; sellAsset(e, amount, receiver); - uint256 exposureCap = getExposureCap(e); - uint256 currentExposure = getCurrentExposure(e); + uint128 exposureCap = getExposureCap(e); + uint128 currentExposure = getCurrentExposure(e); assert currentExposure <= exposureCap; } @@ -176,10 +176,10 @@ rule whoCanChangeExposure(method f) env e; feeLimits(e); priceLimits(e); - uint256 exposureBefore = getCurrentExposure(e); + uint128 exposureBefore = getCurrentExposure(e); calldataarg args; f(e, args); - uint256 exposureAfter = getCurrentExposure(e); + uint128 exposureAfter = getCurrentExposure(e); assert exposureAfter > exposureBefore => canIncreaseExposure(f), "should not increase exposure"; assert exposureAfter < exposureBefore => canDecreaseExposure(f), "should not decrease exposure"; }