From 7ea7192c9dab726520ba6345c7679dd85506b718 Mon Sep 17 00:00:00 2001 From: nisnislevi Date: Sun, 17 Mar 2024 16:17:31 +0200 Subject: [PATCH] for PR --- .github/workflows/certora-steward.yml | 51 ++ .../mutations/mutants/Gsm/Gsm.sol0 copy.sol | 561 ++++++++++++++++++ .../GSM/mutations/mutants/Gsm/Gsm.sol0.sol | 558 +++++++++++++++++ .../mutations/mutants/Gsm/Gsm.sol1 copy.sol | 561 ++++++++++++++++++ .../GSM/mutations/mutants/Gsm/Gsm.sol1.sol | 561 ++++++++++++++++++ .../mutations/mutants/Gsm/Gsm.sol2 copy.sol | 561 ++++++++++++++++++ .../GSM/mutations/mutants/Gsm/Gsm.sol2.sol | 561 ++++++++++++++++++ .../mutations/mutants/Gsm/Gsm.sol3 copy.sol | 561 ++++++++++++++++++ .../GSM/mutations/mutants/Gsm/Gsm.sol3.sol | 561 ++++++++++++++++++ .../feeStrategy/FixedFeeStrategy.sol14.sol | 71 +++ .../feeStrategy/FixedFeeStrategy.sol16.sol | 75 +++ .../feeStrategy/FixedFeeStrategy.sol17.sol | 75 +++ .../feeStrategy/FixedFeeStrategy.sol9.sol | 75 +++ .../FixedPriceStrategy.sol10 copy 2.sol | 64 ++ .../FixedPriceStrategy.sol10 copy.sol | 64 ++ .../FixedPriceStrategy.sol10.sol | 64 ++ .../FixedPriceStrategy.sol12.sol | 64 ++ .../priceStrategy/FixedPriceStrategy.sol7.sol | 60 ++ .../FixedPriceStrategy.sol9 copy.sol | 64 ++ .../priceStrategy/FixedPriceStrategy.sol9.sol | 64 ++ certora/steward/conf/rules.conf | 32 + certora/steward/conf/sanity.conf | 33 ++ .../steward/harness/GhoStewardV2_Harness.sol | 22 + certora/steward/specs/rules.spec | 347 +++++++++++ 24 files changed, 5710 insertions(+) create mode 100644 .github/workflows/certora-steward.yml create mode 100644 certora/GSM/mutations/mutants/Gsm/Gsm.sol0 copy.sol create mode 100644 certora/GSM/mutations/mutants/Gsm/Gsm.sol0.sol create mode 100644 certora/GSM/mutations/mutants/Gsm/Gsm.sol1 copy.sol create mode 100644 certora/GSM/mutations/mutants/Gsm/Gsm.sol1.sol create mode 100644 certora/GSM/mutations/mutants/Gsm/Gsm.sol2 copy.sol create mode 100644 certora/GSM/mutations/mutants/Gsm/Gsm.sol2.sol create mode 100644 certora/GSM/mutations/mutants/Gsm/Gsm.sol3 copy.sol create mode 100644 certora/GSM/mutations/mutants/Gsm/Gsm.sol3.sol create mode 100644 certora/GSM/mutations/mutants/feeStrategy/FixedFeeStrategy.sol14.sol create mode 100644 certora/GSM/mutations/mutants/feeStrategy/FixedFeeStrategy.sol16.sol create mode 100644 certora/GSM/mutations/mutants/feeStrategy/FixedFeeStrategy.sol17.sol create mode 100644 certora/GSM/mutations/mutants/feeStrategy/FixedFeeStrategy.sol9.sol create mode 100644 certora/GSM/mutations/mutants/priceStrategy/FixedPriceStrategy.sol10 copy 2.sol create mode 100644 certora/GSM/mutations/mutants/priceStrategy/FixedPriceStrategy.sol10 copy.sol create mode 100644 certora/GSM/mutations/mutants/priceStrategy/FixedPriceStrategy.sol10.sol create mode 100644 certora/GSM/mutations/mutants/priceStrategy/FixedPriceStrategy.sol12.sol create mode 100644 certora/GSM/mutations/mutants/priceStrategy/FixedPriceStrategy.sol7.sol create mode 100644 certora/GSM/mutations/mutants/priceStrategy/FixedPriceStrategy.sol9 copy.sol create mode 100644 certora/GSM/mutations/mutants/priceStrategy/FixedPriceStrategy.sol9.sol create mode 100644 certora/steward/conf/rules.conf create mode 100644 certora/steward/conf/sanity.conf create mode 100644 certora/steward/harness/GhoStewardV2_Harness.sol create mode 100644 certora/steward/specs/rules.spec diff --git a/.github/workflows/certora-steward.yml b/.github/workflows/certora-steward.yml new file mode 100644 index 00000000..adeac1f8 --- /dev/null +++ b/.github/workflows/certora-steward.yml @@ -0,0 +1,51 @@ +name: certora-steward + +on: + push: + branches: + - main + pull_request: + branches: + - main + + workflow_dispatch: + +jobs: + verify: + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v2 + with: + submodules: recursive + + - name: Install python + uses: actions/setup-python@v2 + with: { python-version: 3.9 } + + - name: Install java + uses: actions/setup-java@v1 + with: { java-version: '11', java-package: jre } + + - name: Install certora cli + run: pip install certora-cli + + - name: Install solc + run: | + wget https://github.com/ethereum/solidity/releases/download/v0.8.10/solc-static-linux + chmod +x solc-static-linux + sudo mv solc-static-linux /usr/local/bin/solc8.10 + + - name: Verify rule ${{ matrix.rule }} + run: | + echo "key length" ${#CERTORAKEY} + certoraRun certora/steward/conf/${{ matrix.rule }} + env: + CERTORAKEY: ${{ secrets.CERTORAKEY }} + + strategy: + fail-fast: false + max-parallel: 16 + matrix: + rule: + - rules.conf diff --git a/certora/GSM/mutations/mutants/Gsm/Gsm.sol0 copy.sol b/certora/GSM/mutations/mutants/Gsm/Gsm.sol0 copy.sol new file mode 100644 index 00000000..f0739a91 --- /dev/null +++ b/certora/GSM/mutations/mutants/Gsm/Gsm.sol0 copy.sol @@ -0,0 +1,561 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.10; + +import {VersionedInitializable} from '@aave/core-v3/contracts/protocol/libraries/aave-upgradeability/VersionedInitializable.sol'; +import {IERC20} from '@aave/core-v3/contracts/dependencies/openzeppelin/contracts/IERC20.sol'; +import {GPv2SafeERC20} from '@aave/core-v3/contracts/dependencies/gnosis/contracts/GPv2SafeERC20.sol'; +import {EIP712} from '@openzeppelin/contracts/utils/cryptography/EIP712.sol'; +import {SignatureChecker} from '@openzeppelin/contracts/utils/cryptography/SignatureChecker.sol'; +import {SafeCast} from '@openzeppelin/contracts/utils/math/SafeCast.sol'; +import {AccessControl} from '@openzeppelin/contracts/access/AccessControl.sol'; +import {IGhoFacilitator} from '../../gho/interfaces/IGhoFacilitator.sol'; +import {IGhoToken} from '../../gho/interfaces/IGhoToken.sol'; +import {IGsmPriceStrategy} from './priceStrategy/interfaces/IGsmPriceStrategy.sol'; +import {IGsmFeeStrategy} from './feeStrategy/interfaces/IGsmFeeStrategy.sol'; +import {IGsm} from './interfaces/IGsm.sol'; + +/** + * @title Gsm + * @author Aave + * @notice GHO Stability Module. It provides buy/sell facilities to go to/from an underlying asset to/from GHO. + * @dev To be covered by a proxy contract. + */ +contract Gsm is AccessControl, VersionedInitializable, EIP712, IGsm { + using GPv2SafeERC20 for IERC20; + using SafeCast for uint256; + + /// @inheritdoc IGsm + bytes32 public constant CONFIGURATOR_ROLE = keccak256('CONFIGURATOR_ROLE'); + + /// @inheritdoc IGsm + bytes32 public constant TOKEN_RESCUER_ROLE = keccak256('TOKEN_RESCUER_ROLE'); + + /// @inheritdoc IGsm + bytes32 public constant SWAP_FREEZER_ROLE = keccak256('SWAP_FREEZER_ROLE'); + + /// @inheritdoc IGsm + bytes32 public constant LIQUIDATOR_ROLE = keccak256('LIQUIDATOR_ROLE'); + + /// @inheritdoc IGsm + bytes32 public constant BUY_ASSET_WITH_SIG_TYPEHASH = + keccak256( + 'BuyAssetWithSig(address originator,uint256 minAmount,address receiver,uint256 nonce,uint256 deadline)' + ); + + /// @inheritdoc IGsm + bytes32 public constant SELL_ASSET_WITH_SIG_TYPEHASH = + keccak256( + 'SellAssetWithSig(address originator,uint256 maxAmount,address receiver,uint256 nonce,uint256 deadline)' + ); + + /// @inheritdoc IGsm + address public immutable GHO_TOKEN; + + /// @inheritdoc IGsm + address public immutable UNDERLYING_ASSET; + + /// @inheritdoc IGsm + address public immutable PRICE_STRATEGY; + + /// @inheritdoc IGsm + mapping(address => uint256) public nonces; + + address internal _ghoTreasury; + address internal _feeStrategy; + bool internal _isFrozen; + bool internal _isSeized; + uint128 internal _exposureCap; + uint128 internal _currentExposure; + uint128 internal _accruedFees; + + /** + * @dev Require GSM to not be frozen for functions marked by this modifier + */ + modifier notFrozen() { + require(!_isFrozen, 'GSM_FROZEN'); + _; + } + + /** + * @dev Require GSM to not be seized for functions marked by this modifier + */ + modifier notSeized() { + require(!_isSeized, 'GSM_SEIZED'); + _; + } + + /** + * @dev Constructor + * @param ghoToken The address of the GHO token contract + * @param underlyingAsset The address of the collateral asset + * @param priceStrategy The address of the price strategy + */ + constructor(address ghoToken, address underlyingAsset, address priceStrategy) EIP712('GSM', '1') { + /// RequireMutation of: require(ghoToken != address(0), 'ZERO_ADDRESS_NOT_VALID'); + require(!(ghoToken != address(0)), 'ZERO_ADDRESS_NOT_VALID'); + require(underlyingAsset != address(0), 'ZERO_ADDRESS_NOT_VALID'); + require( + IGsmPriceStrategy(priceStrategy).UNDERLYING_ASSET() == underlyingAsset, + 'INVALID_PRICE_STRATEGY' + ); + GHO_TOKEN = ghoToken; + UNDERLYING_ASSET = underlyingAsset; + PRICE_STRATEGY = priceStrategy; + } + + /** + * @notice GSM initializer + * @param admin The address of the default admin role + * @param ghoTreasury The address of the GHO treasury + * @param exposureCap Maximum amount of user-supplied underlying asset in GSM + */ + function initialize( + address admin, + address ghoTreasury, + uint128 exposureCap + ) external initializer { + require(admin != address(0), 'ZERO_ADDRESS_NOT_VALID'); + _grantRole(DEFAULT_ADMIN_ROLE, admin); + _grantRole(CONFIGURATOR_ROLE, admin); + _updateGhoTreasury(ghoTreasury); + _updateExposureCap(exposureCap); + } + + /// @inheritdoc IGsm + function buyAsset( + uint256 minAmount, + address receiver + ) external notFrozen notSeized returns (uint256, uint256) { + return _buyAsset(msg.sender, minAmount, receiver); + } + + /// @inheritdoc IGsm + function buyAssetWithSig( + address originator, + uint256 minAmount, + address receiver, + uint256 deadline, + bytes calldata signature + ) external notFrozen notSeized returns (uint256, uint256) { + require(deadline >= block.timestamp, 'SIGNATURE_DEADLINE_EXPIRED'); + bytes32 digest = keccak256( + abi.encode( + '\x19\x01', + _domainSeparatorV4(), + BUY_ASSET_WITH_SIG_TYPEHASH, + abi.encode(originator, minAmount, receiver, nonces[originator]++, deadline) + ) + ); + require( + SignatureChecker.isValidSignatureNow(originator, digest, signature), + 'SIGNATURE_INVALID' + ); + + return _buyAsset(originator, minAmount, receiver); + } + + /// @inheritdoc IGsm + function sellAsset( + uint256 maxAmount, + address receiver + ) external notFrozen notSeized returns (uint256, uint256) { + return _sellAsset(msg.sender, maxAmount, receiver); + } + + /// @inheritdoc IGsm + function sellAssetWithSig( + address originator, + uint256 maxAmount, + address receiver, + uint256 deadline, + bytes calldata signature + ) external notFrozen notSeized returns (uint256, uint256) { + require(deadline >= block.timestamp, 'SIGNATURE_DEADLINE_EXPIRED'); + bytes32 digest = keccak256( + abi.encode( + '\x19\x01', + _domainSeparatorV4(), + SELL_ASSET_WITH_SIG_TYPEHASH, + abi.encode(originator, maxAmount, receiver, nonces[originator]++, deadline) + ) + ); + require( + SignatureChecker.isValidSignatureNow(originator, digest, signature), + 'SIGNATURE_INVALID' + ); + + return _sellAsset(originator, maxAmount, receiver); + } + + /// @inheritdoc IGsm + function rescueTokens( + address token, + address to, + uint256 amount + ) external onlyRole(TOKEN_RESCUER_ROLE) { + require(amount > 0, 'INVALID_AMOUNT'); + if (token == GHO_TOKEN) { + uint256 rescuableBalance = IERC20(token).balanceOf(address(this)) - _accruedFees; + require(rescuableBalance >= amount, 'INSUFFICIENT_GHO_TO_RESCUE'); + } + if (token == UNDERLYING_ASSET) { + uint256 rescuableBalance = IERC20(token).balanceOf(address(this)) - _currentExposure; + require(rescuableBalance >= amount, 'INSUFFICIENT_EXOGENOUS_ASSET_TO_RESCUE'); + } + IERC20(token).safeTransfer(to, amount); + emit TokensRescued(token, to, amount); + } + + /// @inheritdoc IGsm + function setSwapFreeze(bool enable) external onlyRole(SWAP_FREEZER_ROLE) { + if (enable) { + require(!_isFrozen, 'GSM_ALREADY_FROZEN'); + } else { + require(_isFrozen, 'GSM_ALREADY_UNFROZEN'); + } + _isFrozen = enable; + emit SwapFreeze(msg.sender, enable); + } + + /// @inheritdoc IGsm + function seize() external notSeized onlyRole(LIQUIDATOR_ROLE) returns (uint256) { + _isSeized = true; + _currentExposure = 0; + _updateExposureCap(0); + + (, uint256 ghoMinted) = IGhoToken(GHO_TOKEN).getFacilitatorBucket(address(this)); + uint256 underlyingBalance = IERC20(UNDERLYING_ASSET).balanceOf(address(this)); + if (underlyingBalance > 0) { + IERC20(UNDERLYING_ASSET).safeTransfer(_ghoTreasury, underlyingBalance); + } + + emit Seized(msg.sender, _ghoTreasury, underlyingBalance, ghoMinted); + return underlyingBalance; + } + + /// @inheritdoc IGsm + function burnAfterSeize(uint256 amount) external onlyRole(LIQUIDATOR_ROLE) returns (uint256) { + require(_isSeized, 'GSM_NOT_SEIZED'); + require(amount > 0, 'INVALID_AMOUNT'); + + (, uint256 ghoMinted) = IGhoToken(GHO_TOKEN).getFacilitatorBucket(address(this)); + if (amount > ghoMinted) { + amount = ghoMinted; + } + IGhoToken(GHO_TOKEN).transferFrom(msg.sender, address(this), amount); + IGhoToken(GHO_TOKEN).burn(amount); + + emit BurnAfterSeize(msg.sender, amount, (ghoMinted - amount)); + return amount; + } + + /// @inheritdoc IGsm + function updateFeeStrategy(address feeStrategy) external onlyRole(CONFIGURATOR_ROLE) { + _updateFeeStrategy(feeStrategy); + } + + /// @inheritdoc IGsm + function updateExposureCap(uint128 exposureCap) external onlyRole(CONFIGURATOR_ROLE) { + _updateExposureCap(exposureCap); + } + + /// @inheritdoc IGhoFacilitator + function distributeFeesToTreasury() public virtual override { + uint256 accruedFees = _accruedFees; + if (accruedFees > 0) { + _accruedFees = 0; + IERC20(GHO_TOKEN).transfer(_ghoTreasury, accruedFees); + emit FeesDistributedToTreasury(_ghoTreasury, GHO_TOKEN, accruedFees); + } + } + + /// @inheritdoc IGhoFacilitator + function updateGhoTreasury(address newGhoTreasury) external override onlyRole(CONFIGURATOR_ROLE) { + _updateGhoTreasury(newGhoTreasury); + } + + /// @inheritdoc IGsm + function DOMAIN_SEPARATOR() external view returns (bytes32) { + return _domainSeparatorV4(); + } + + /// @inheritdoc IGsm + function getGhoAmountForBuyAsset( + uint256 minAssetAmount + ) external view returns (uint256, uint256, uint256, uint256) { + return _calculateGhoAmountForBuyAsset(minAssetAmount); + } + + /// @inheritdoc IGsm + function getGhoAmountForSellAsset( + uint256 maxAssetAmount + ) external view returns (uint256, uint256, uint256, uint256) { + return _calculateGhoAmountForSellAsset(maxAssetAmount); + } + + /// @inheritdoc IGsm + function getAssetAmountForBuyAsset( + uint256 maxGhoAmount + ) external view returns (uint256, uint256, uint256, uint256) { + bool withFee = _feeStrategy != address(0); + uint256 grossAmount = withFee + ? IGsmFeeStrategy(_feeStrategy).getGrossAmountFromTotalBought(maxGhoAmount) + : maxGhoAmount; + // round down so maxGhoAmount is guaranteed + uint256 assetAmount = IGsmPriceStrategy(PRICE_STRATEGY).getGhoPriceInAsset(grossAmount, false); + uint256 finalGrossAmount = IGsmPriceStrategy(PRICE_STRATEGY).getAssetPriceInGho( + assetAmount, + true // TODO + ); + uint256 finalFee = withFee ? IGsmFeeStrategy(_feeStrategy).getBuyFee(finalGrossAmount) : 0; + return (assetAmount, finalGrossAmount + finalFee, finalGrossAmount, finalFee); + } + + /// @inheritdoc IGsm + function getAssetAmountForSellAsset( + uint256 minGhoAmount + ) external view returns (uint256, uint256, uint256, uint256) { + bool withFee = _feeStrategy != address(0); + uint256 grossAmount = withFee + ? IGsmFeeStrategy(_feeStrategy).getGrossAmountFromTotalSold(minGhoAmount) + : minGhoAmount; + // round up so minGhoAmount is guaranteed + uint256 assetAmount = IGsmPriceStrategy(PRICE_STRATEGY).getGhoPriceInAsset(grossAmount, true); + uint256 finalGrossAmount = IGsmPriceStrategy(PRICE_STRATEGY).getAssetPriceInGho( + assetAmount, + false // TODO + ); + uint256 finalFee = withFee ? IGsmFeeStrategy(_feeStrategy).getSellFee(finalGrossAmount) : 0; + return (assetAmount, finalGrossAmount - finalFee, finalGrossAmount, finalFee); + } + + /// @inheritdoc IGsm + function getAvailableUnderlyingExposure() external view returns (uint256) { + return _exposureCap > _currentExposure ? _exposureCap - _currentExposure : 0; + } + + /// @inheritdoc IGsm + function getAvailableLiquidity() external view returns (uint256) { + return _currentExposure; + } + + /// @inheritdoc IGsm + function getFeeStrategy() external view returns (address) { + return _feeStrategy; + } + + /// @inheritdoc IGsm + function getAccruedFees() external view returns (uint256) { + return _accruedFees; + } + + /// @inheritdoc IGsm + function getIsFrozen() external view returns (bool) { + return _isFrozen; + } + + /// @inheritdoc IGsm + function getIsSeized() external view returns (bool) { + return _isSeized; + } + + /// @inheritdoc IGsm + function canSwap() external view returns (bool) { + return !_isFrozen && !_isSeized; + } + + /// @inheritdoc IGhoFacilitator + function getGhoTreasury() external view override returns (address) { + return _ghoTreasury; + } + + /// @inheritdoc IGsm + function GSM_REVISION() public pure virtual override returns (uint256) { + return 1; + } + + /** + * @dev Buys an underlying asset with GHO + * @param originator The originator of the request + * @param minAmount The minimum amount of the underlying asset desired for purchase + * @param receiver The recipient address of the underlying asset being purchased + * @return The amount of underlying asset bought + * @return The amount of GHO sold by the user + */ + function _buyAsset( + address originator, + uint256 minAmount, + address receiver + ) internal returns (uint256, uint256) { + ( + uint256 assetAmount, + uint256 ghoSold, + uint256 grossAmount, + uint256 fee + ) = _calculateGhoAmountForBuyAsset(minAmount); + + _beforeBuyAsset(originator, assetAmount, receiver); + + require(assetAmount > 0, 'INVALID_AMOUNT'); + require(_currentExposure >= assetAmount, 'INSUFFICIENT_AVAILABLE_EXOGENOUS_ASSET_LIQUIDITY'); + + _currentExposure -= uint128(assetAmount); + _accruedFees += fee.toUint128(); + IGhoToken(GHO_TOKEN).transferFrom(originator, address(this), ghoSold); + IGhoToken(GHO_TOKEN).burn(grossAmount); + IERC20(UNDERLYING_ASSET).safeTransfer(receiver, assetAmount); + + emit BuyAsset(originator, receiver, assetAmount, ghoSold, fee); + return (assetAmount, ghoSold); + } + + /** + * @dev Hook that is called before `buyAsset`. + * @dev This can be used to add custom logic + * @param originator Originator of the request + * @param amount The amount of the underlying asset desired for purchase + * @param receiver Recipient address of the underlying asset being purchased + */ + function _beforeBuyAsset(address originator, uint256 amount, address receiver) internal virtual {} + + /** + * @dev Sells an underlying asset for GHO + * @param originator The originator of the request + * @param maxAmount The maximum amount of the underlying asset desired to sell + * @param receiver The recipient address of the GHO being purchased + * @return The amount of underlying asset sold + * @return The amount of GHO bought by the user + */ + function _sellAsset( + address originator, + uint256 maxAmount, + address receiver + ) internal returns (uint256, uint256) { + ( + uint256 assetAmount, + uint256 ghoBought, + uint256 grossAmount, + uint256 fee + ) = _calculateGhoAmountForSellAsset(maxAmount); + + _beforeSellAsset(originator, assetAmount, receiver); + + require(assetAmount > 0, 'INVALID_AMOUNT'); + require(_currentExposure + assetAmount <= _exposureCap, 'EXOGENOUS_ASSET_EXPOSURE_TOO_HIGH'); + + _currentExposure += uint128(assetAmount); + _accruedFees += fee.toUint128(); + IERC20(UNDERLYING_ASSET).safeTransferFrom(originator, address(this), assetAmount); + + IGhoToken(GHO_TOKEN).mint(address(this), grossAmount); + IGhoToken(GHO_TOKEN).transfer(receiver, ghoBought); + + emit SellAsset(originator, receiver, assetAmount, grossAmount, fee); + return (assetAmount, ghoBought); + } + + /** + * @dev Hook that is called before `sellAsset`. + * @dev This can be used to add custom logic + * @param originator Originator of the request + * @param amount The amount of the underlying asset desired to sell + * @param receiver Recipient address of the GHO being purchased + */ + function _beforeSellAsset( + address originator, + uint256 amount, + address receiver + ) internal virtual {} + + /** + * @dev Returns the amount of GHO sold in exchange of buying underlying asset + * @param assetAmount The amount of underlying asset to buy + * @return The exact amount of asset the user purchases + * @return The total amount of GHO the user sells (gross amount in GHO plus fee) + * @return The gross amount of GHO + * @return The fee amount in GHO, applied on top of gross amount of GHO + */ + function _calculateGhoAmountForBuyAsset( + uint256 assetAmount + ) internal view returns (uint256, uint256, uint256, uint256) { + bool withFee = _feeStrategy != address(0); + // pick the highest GHO amount possible for given asset amount + uint256 grossAmount = IGsmPriceStrategy(PRICE_STRATEGY).getAssetPriceInGho(assetAmount, true); + uint256 fee = withFee ? IGsmFeeStrategy(_feeStrategy).getBuyFee(grossAmount) : 0; + uint256 ghoSold = grossAmount + fee; + uint256 finalGrossAmount = withFee + ? IGsmFeeStrategy(_feeStrategy).getGrossAmountFromTotalBought(ghoSold) + : ghoSold; + // pick the lowest asset amount possible for given GHO amount + uint256 finalAssetAmount = IGsmPriceStrategy(PRICE_STRATEGY).getGhoPriceInAsset( + finalGrossAmount, + false + ); + uint256 finalFee = ghoSold - finalGrossAmount; + return (finalAssetAmount, finalGrossAmount + finalFee, finalGrossAmount, finalFee); + } + + /** + * @dev Returns the amount of GHO bought in exchange of a given amount of underlying asset + * @param assetAmount The amount of underlying asset to sell + * @return The exact amount of asset the user sells + * @return The total amount of GHO the user buys (gross amount in GHO minus fee) + * @return The gross amount of GHO + * @return The fee amount in GHO, applied to the gross amount of GHO + */ + function _calculateGhoAmountForSellAsset( + uint256 assetAmount + ) internal view returns (uint256, uint256, uint256, uint256) { + bool withFee = _feeStrategy != address(0); + // pick the lowest GHO amount possible for given asset amount + uint256 grossAmount = IGsmPriceStrategy(PRICE_STRATEGY).getAssetPriceInGho(assetAmount, false); + uint256 fee = withFee ? IGsmFeeStrategy(_feeStrategy).getSellFee(grossAmount) : 0; + uint256 ghoBought = grossAmount - fee; + uint256 finalGrossAmount = withFee + ? IGsmFeeStrategy(_feeStrategy).getGrossAmountFromTotalSold(ghoBought) + : ghoBought; + // pick the highest asset amount possible for given GHO amount + uint256 finalAssetAmount = IGsmPriceStrategy(PRICE_STRATEGY).getGhoPriceInAsset( + finalGrossAmount, + true + ); + uint256 finalFee = finalGrossAmount - ghoBought; + return (finalAssetAmount, finalGrossAmount - finalFee, finalGrossAmount, finalFee); + } + + /** + * @dev Updates Fee Strategy + * @param feeStrategy The address of the new Fee Strategy + */ + function _updateFeeStrategy(address feeStrategy) internal { + address oldFeeStrategy = _feeStrategy; + _feeStrategy = feeStrategy; + emit FeeStrategyUpdated(oldFeeStrategy, feeStrategy); + } + + /** + * @dev Updates Exposure Cap + * @param exposureCap The value of the new Exposure Cap + */ + function _updateExposureCap(uint128 exposureCap) internal { + uint128 oldExposureCap = _exposureCap; + _exposureCap = exposureCap; + emit ExposureCapUpdated(oldExposureCap, exposureCap); + } + + /** + * @dev Updates GHO Treasury Address + * @param newGhoTreasury The address of the new GHO Treasury + */ + function _updateGhoTreasury(address newGhoTreasury) internal { + require(newGhoTreasury != address(0), 'ZERO_ADDRESS_NOT_VALID'); + address oldGhoTreasury = _ghoTreasury; + _ghoTreasury = newGhoTreasury; + emit GhoTreasuryUpdated(oldGhoTreasury, newGhoTreasury); + } + + /// @inheritdoc VersionedInitializable + function getRevision() internal pure virtual override returns (uint256) { + return GSM_REVISION(); + } +} diff --git a/certora/GSM/mutations/mutants/Gsm/Gsm.sol0.sol b/certora/GSM/mutations/mutants/Gsm/Gsm.sol0.sol new file mode 100644 index 00000000..6e67153f --- /dev/null +++ b/certora/GSM/mutations/mutants/Gsm/Gsm.sol0.sol @@ -0,0 +1,558 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.10; + +import {VersionedInitializable} from '@aave/core-v3/contracts/protocol/libraries/aave-upgradeability/VersionedInitializable.sol'; +import {IERC20} from '@aave/core-v3/contracts/dependencies/openzeppelin/contracts/IERC20.sol'; +import {GPv2SafeERC20} from '@aave/core-v3/contracts/dependencies/gnosis/contracts/GPv2SafeERC20.sol'; +import {EIP712} from '@openzeppelin/contracts/utils/cryptography/EIP712.sol'; +import {SignatureChecker} from '@openzeppelin/contracts/utils/cryptography/SignatureChecker.sol'; +import {SafeCast} from '@openzeppelin/contracts/utils/math/SafeCast.sol'; +import {AccessControl} from '@openzeppelin/contracts/access/AccessControl.sol'; +import {IGhoFacilitator} from '../../gho/interfaces/IGhoFacilitator.sol'; +import {IGhoToken} from '../../gho/interfaces/IGhoToken.sol'; +import {IGsmPriceStrategy} from './priceStrategy/interfaces/IGsmPriceStrategy.sol'; +import {IGsmFeeStrategy} from './feeStrategy/interfaces/IGsmFeeStrategy.sol'; +import {IGsm} from './interfaces/IGsm.sol'; + +/** + * @title Gsm + * @author Aave + * @notice GHO Stability Module. It provides buy/sell facilities to go to/from an underlying asset to/from GHO. + * @dev To be covered by a proxy contract. + */ +contract Gsm is AccessControl, VersionedInitializable, EIP712, IGsm { + using GPv2SafeERC20 for IERC20; + using SafeCast for uint256; + + /// @inheritdoc IGsm + bytes32 public constant CONFIGURATOR_ROLE = keccak256('CONFIGURATOR_ROLE'); + + /// @inheritdoc IGsm + bytes32 public constant TOKEN_RESCUER_ROLE = keccak256('TOKEN_RESCUER_ROLE'); + + /// @inheritdoc IGsm + bytes32 public constant SWAP_FREEZER_ROLE = keccak256('SWAP_FREEZER_ROLE'); + + /// @inheritdoc IGsm + bytes32 public constant LIQUIDATOR_ROLE = keccak256('LIQUIDATOR_ROLE'); + + /// @inheritdoc IGsm + bytes32 public constant BUY_ASSET_WITH_SIG_TYPEHASH = + keccak256( + 'BuyAssetWithSig(address originator,uint256 minAmount,address receiver,uint256 nonce,uint256 deadline)' + ); + + /// @inheritdoc IGsm + bytes32 public constant SELL_ASSET_WITH_SIG_TYPEHASH = + keccak256( + 'SellAssetWithSig(address originator,uint256 maxAmount,address receiver,uint256 nonce,uint256 deadline)' + ); + + /// @inheritdoc IGsm + address public immutable GHO_TOKEN; + + /// @inheritdoc IGsm + address public immutable UNDERLYING_ASSET; + + /// @inheritdoc IGsm + address public immutable PRICE_STRATEGY; + + /// @inheritdoc IGsm + mapping(address => uint256) public nonces; + + address internal _ghoTreasury; + address internal _feeStrategy; + bool internal _isFrozen; + bool internal _isSeized; + uint128 internal _exposureCap; + uint128 internal _currentExposure; + uint128 internal _accruedFees; + + /** + * @dev Require GSM to not be frozen for functions marked by this modifier + */ + modifier notFrozen() { + require(!_isFrozen, 'GSM_FROZEN'); + _; + } + + /** + * @dev Require GSM to not be seized for functions marked by this modifier + */ + modifier notSeized() { + require(!_isSeized, 'GSM_SEIZED'); + _; + } + + /** + * @dev Constructor + * @param ghoToken The address of the GHO token contract + * @param underlyingAsset The address of the collateral asset + * @param priceStrategy The address of the price strategy + */ + constructor(address ghoToken, address underlyingAsset, address priceStrategy) EIP712('GSM', '1') { + require(ghoToken != address(0), 'ZERO_ADDRESS_NOT_VALID'); + require(underlyingAsset != address(0), 'ZERO_ADDRESS_NOT_VALID'); + require( + IGsmPriceStrategy(priceStrategy).UNDERLYING_ASSET() == underlyingAsset, + 'INVALID_PRICE_STRATEGY' + ); + GHO_TOKEN = ghoToken; + UNDERLYING_ASSET = underlyingAsset; + PRICE_STRATEGY = priceStrategy; + } + + /** + * @notice GSM initializer + * @param admin The address of the default admin role + * @param ghoTreasury The address of the GHO treasury + * @param exposureCap Maximum amount of user-supplied underlying asset in GSM + */ + function initialize( + address admin, + address ghoTreasury, + uint128 exposureCap + ) external initializer { + require(admin != address(0), 'ZERO_ADDRESS_NOT_VALID'); + _grantRole(DEFAULT_ADMIN_ROLE, admin); + _grantRole(CONFIGURATOR_ROLE, admin); + _updateGhoTreasury(ghoTreasury); + _updateExposureCap(exposureCap); + } + + /// @inheritdoc IGsm + function buyAsset( + uint256 minAmount, + address receiver + ) external notFrozen notSeized returns (uint256, uint256) { + return _buyAsset(msg.sender, minAmount, receiver); + } + + /// @inheritdoc IGsm + function buyAssetWithSig( + address originator, + uint256 minAmount, + address receiver, + uint256 deadline, + bytes calldata signature + ) external notFrozen notSeized returns (uint256, uint256) { + require(deadline >= block.timestamp, 'SIGNATURE_DEADLINE_EXPIRED'); + bytes32 digest = keccak256( + abi.encode( + '\x19\x01', + _domainSeparatorV4(), + BUY_ASSET_WITH_SIG_TYPEHASH, + abi.encode(originator, minAmount, receiver, nonces[originator]++, deadline) + ) + ); + /// FunctionCallMutation of: require( + SignatureChecker.isValidSignatureNow(originator, digest, signature); + + return _buyAsset(originator, minAmount, receiver); + } + + /// @inheritdoc IGsm + function sellAsset( + uint256 maxAmount, + address receiver + ) external notFrozen notSeized returns (uint256, uint256) { + return _sellAsset(msg.sender, maxAmount, receiver); + } + + /// @inheritdoc IGsm + function sellAssetWithSig( + address originator, + uint256 maxAmount, + address receiver, + uint256 deadline, + bytes calldata signature + ) external notFrozen notSeized returns (uint256, uint256) { + require(deadline >= block.timestamp, 'SIGNATURE_DEADLINE_EXPIRED'); + bytes32 digest = keccak256( + abi.encode( + '\x19\x01', + _domainSeparatorV4(), + SELL_ASSET_WITH_SIG_TYPEHASH, + abi.encode(originator, maxAmount, receiver, nonces[originator]++, deadline) + ) + ); + require( + SignatureChecker.isValidSignatureNow(originator, digest, signature), + 'SIGNATURE_INVALID' + ); + + return _sellAsset(originator, maxAmount, receiver); + } + + /// @inheritdoc IGsm + function rescueTokens( + address token, + address to, + uint256 amount + ) external onlyRole(TOKEN_RESCUER_ROLE) { + require(amount > 0, 'INVALID_AMOUNT'); + if (token == GHO_TOKEN) { + uint256 rescuableBalance = IERC20(token).balanceOf(address(this)) - _accruedFees; + require(rescuableBalance >= amount, 'INSUFFICIENT_GHO_TO_RESCUE'); + } + if (token == UNDERLYING_ASSET) { + uint256 rescuableBalance = IERC20(token).balanceOf(address(this)) - _currentExposure; + require(rescuableBalance >= amount, 'INSUFFICIENT_EXOGENOUS_ASSET_TO_RESCUE'); + } + IERC20(token).safeTransfer(to, amount); + emit TokensRescued(token, to, amount); + } + + /// @inheritdoc IGsm + function setSwapFreeze(bool enable) external onlyRole(SWAP_FREEZER_ROLE) { + if (enable) { + require(!_isFrozen, 'GSM_ALREADY_FROZEN'); + } else { + require(_isFrozen, 'GSM_ALREADY_UNFROZEN'); + } + _isFrozen = enable; + emit SwapFreeze(msg.sender, enable); + } + + /// @inheritdoc IGsm + function seize() external notSeized onlyRole(LIQUIDATOR_ROLE) returns (uint256) { + _isSeized = true; + _currentExposure = 0; + _updateExposureCap(0); + + (, uint256 ghoMinted) = IGhoToken(GHO_TOKEN).getFacilitatorBucket(address(this)); + uint256 underlyingBalance = IERC20(UNDERLYING_ASSET).balanceOf(address(this)); + if (underlyingBalance > 0) { + IERC20(UNDERLYING_ASSET).safeTransfer(_ghoTreasury, underlyingBalance); + } + + emit Seized(msg.sender, _ghoTreasury, underlyingBalance, ghoMinted); + return underlyingBalance; + } + + /// @inheritdoc IGsm + function burnAfterSeize(uint256 amount) external onlyRole(LIQUIDATOR_ROLE) returns (uint256) { + require(_isSeized, 'GSM_NOT_SEIZED'); + require(amount > 0, 'INVALID_AMOUNT'); + + (, uint256 ghoMinted) = IGhoToken(GHO_TOKEN).getFacilitatorBucket(address(this)); + if (amount > ghoMinted) { + amount = ghoMinted; + } + IGhoToken(GHO_TOKEN).transferFrom(msg.sender, address(this), amount); + IGhoToken(GHO_TOKEN).burn(amount); + + emit BurnAfterSeize(msg.sender, amount, (ghoMinted - amount)); + return amount; + } + + /// @inheritdoc IGsm + function updateFeeStrategy(address feeStrategy) external onlyRole(CONFIGURATOR_ROLE) { + _updateFeeStrategy(feeStrategy); + } + + /// @inheritdoc IGsm + function updateExposureCap(uint128 exposureCap) external onlyRole(CONFIGURATOR_ROLE) { + _updateExposureCap(exposureCap); + } + + /// @inheritdoc IGhoFacilitator + function distributeFeesToTreasury() public virtual override { + uint256 accruedFees = _accruedFees; + if (accruedFees > 0) { + _accruedFees = 0; + IERC20(GHO_TOKEN).transfer(_ghoTreasury, accruedFees); + emit FeesDistributedToTreasury(_ghoTreasury, GHO_TOKEN, accruedFees); + } + } + + /// @inheritdoc IGhoFacilitator + function updateGhoTreasury(address newGhoTreasury) external override onlyRole(CONFIGURATOR_ROLE) { + _updateGhoTreasury(newGhoTreasury); + } + + /// @inheritdoc IGsm + function DOMAIN_SEPARATOR() external view returns (bytes32) { + return _domainSeparatorV4(); + } + + /// @inheritdoc IGsm + function getGhoAmountForBuyAsset( + uint256 minAssetAmount + ) external view returns (uint256, uint256, uint256, uint256) { + return _calculateGhoAmountForBuyAsset(minAssetAmount); + } + + /// @inheritdoc IGsm + function getGhoAmountForSellAsset( + uint256 maxAssetAmount + ) external view returns (uint256, uint256, uint256, uint256) { + return _calculateGhoAmountForSellAsset(maxAssetAmount); + } + + /// @inheritdoc IGsm + function getAssetAmountForBuyAsset( + uint256 maxGhoAmount + ) external view returns (uint256, uint256, uint256, uint256) { + bool withFee = _feeStrategy != address(0); + uint256 grossAmount = withFee + ? IGsmFeeStrategy(_feeStrategy).getGrossAmountFromTotalBought(maxGhoAmount) + : maxGhoAmount; + // round down so maxGhoAmount is guaranteed + uint256 assetAmount = IGsmPriceStrategy(PRICE_STRATEGY).getGhoPriceInAsset(grossAmount, false); + uint256 finalGrossAmount = IGsmPriceStrategy(PRICE_STRATEGY).getAssetPriceInGho( + assetAmount, + true // TODO + ); + uint256 finalFee = withFee ? IGsmFeeStrategy(_feeStrategy).getBuyFee(finalGrossAmount) : 0; + return (assetAmount, finalGrossAmount + finalFee, finalGrossAmount, finalFee); + } + + /// @inheritdoc IGsm + function getAssetAmountForSellAsset( + uint256 minGhoAmount + ) external view returns (uint256, uint256, uint256, uint256) { + bool withFee = _feeStrategy != address(0); + uint256 grossAmount = withFee + ? IGsmFeeStrategy(_feeStrategy).getGrossAmountFromTotalSold(minGhoAmount) + : minGhoAmount; + // round up so minGhoAmount is guaranteed + uint256 assetAmount = IGsmPriceStrategy(PRICE_STRATEGY).getGhoPriceInAsset(grossAmount, true); + uint256 finalGrossAmount = IGsmPriceStrategy(PRICE_STRATEGY).getAssetPriceInGho( + assetAmount, + false // TODO + ); + uint256 finalFee = withFee ? IGsmFeeStrategy(_feeStrategy).getSellFee(finalGrossAmount) : 0; + return (assetAmount, finalGrossAmount - finalFee, finalGrossAmount, finalFee); + } + + /// @inheritdoc IGsm + function getAvailableUnderlyingExposure() external view returns (uint256) { + return _exposureCap > _currentExposure ? _exposureCap - _currentExposure : 0; + } + + /// @inheritdoc IGsm + function getAvailableLiquidity() external view returns (uint256) { + return _currentExposure; + } + + /// @inheritdoc IGsm + function getFeeStrategy() external view returns (address) { + return _feeStrategy; + } + + /// @inheritdoc IGsm + function getAccruedFees() external view returns (uint256) { + return _accruedFees; + } + + /// @inheritdoc IGsm + function getIsFrozen() external view returns (bool) { + return _isFrozen; + } + + /// @inheritdoc IGsm + function getIsSeized() external view returns (bool) { + return _isSeized; + } + + /// @inheritdoc IGsm + function canSwap() external view returns (bool) { + return !_isFrozen && !_isSeized; + } + + /// @inheritdoc IGhoFacilitator + function getGhoTreasury() external view override returns (address) { + return _ghoTreasury; + } + + /// @inheritdoc IGsm + function GSM_REVISION() public pure virtual override returns (uint256) { + return 1; + } + + /** + * @dev Buys an underlying asset with GHO + * @param originator The originator of the request + * @param minAmount The minimum amount of the underlying asset desired for purchase + * @param receiver The recipient address of the underlying asset being purchased + * @return The amount of underlying asset bought + * @return The amount of GHO sold by the user + */ + function _buyAsset( + address originator, + uint256 minAmount, + address receiver + ) internal returns (uint256, uint256) { + ( + uint256 assetAmount, + uint256 ghoSold, + uint256 grossAmount, + uint256 fee + ) = _calculateGhoAmountForBuyAsset(minAmount); + + _beforeBuyAsset(originator, assetAmount, receiver); + + require(assetAmount > 0, 'INVALID_AMOUNT'); + require(_currentExposure >= assetAmount, 'INSUFFICIENT_AVAILABLE_EXOGENOUS_ASSET_LIQUIDITY'); + + _currentExposure -= uint128(assetAmount); + _accruedFees += fee.toUint128(); + IGhoToken(GHO_TOKEN).transferFrom(originator, address(this), ghoSold); + IGhoToken(GHO_TOKEN).burn(grossAmount); + IERC20(UNDERLYING_ASSET).safeTransfer(receiver, assetAmount); + + emit BuyAsset(originator, receiver, assetAmount, ghoSold, fee); + return (assetAmount, ghoSold); + } + + /** + * @dev Hook that is called before `buyAsset`. + * @dev This can be used to add custom logic + * @param originator Originator of the request + * @param amount The amount of the underlying asset desired for purchase + * @param receiver Recipient address of the underlying asset being purchased + */ + function _beforeBuyAsset(address originator, uint256 amount, address receiver) internal virtual {} + + /** + * @dev Sells an underlying asset for GHO + * @param originator The originator of the request + * @param maxAmount The maximum amount of the underlying asset desired to sell + * @param receiver The recipient address of the GHO being purchased + * @return The amount of underlying asset sold + * @return The amount of GHO bought by the user + */ + function _sellAsset( + address originator, + uint256 maxAmount, + address receiver + ) internal returns (uint256, uint256) { + ( + uint256 assetAmount, + uint256 ghoBought, + uint256 grossAmount, + uint256 fee + ) = _calculateGhoAmountForSellAsset(maxAmount); + + _beforeSellAsset(originator, assetAmount, receiver); + + require(assetAmount > 0, 'INVALID_AMOUNT'); + require(_currentExposure + assetAmount <= _exposureCap, 'EXOGENOUS_ASSET_EXPOSURE_TOO_HIGH'); + + _currentExposure += uint128(assetAmount); + _accruedFees += fee.toUint128(); + IERC20(UNDERLYING_ASSET).safeTransferFrom(originator, address(this), assetAmount); + + IGhoToken(GHO_TOKEN).mint(address(this), grossAmount); + IGhoToken(GHO_TOKEN).transfer(receiver, ghoBought); + + emit SellAsset(originator, receiver, assetAmount, grossAmount, fee); + return (assetAmount, ghoBought); + } + + /** + * @dev Hook that is called before `sellAsset`. + * @dev This can be used to add custom logic + * @param originator Originator of the request + * @param amount The amount of the underlying asset desired to sell + * @param receiver Recipient address of the GHO being purchased + */ + function _beforeSellAsset( + address originator, + uint256 amount, + address receiver + ) internal virtual {} + + /** + * @dev Returns the amount of GHO sold in exchange of buying underlying asset + * @param assetAmount The amount of underlying asset to buy + * @return The exact amount of asset the user purchases + * @return The total amount of GHO the user sells (gross amount in GHO plus fee) + * @return The gross amount of GHO + * @return The fee amount in GHO, applied on top of gross amount of GHO + */ + function _calculateGhoAmountForBuyAsset( + uint256 assetAmount + ) internal view returns (uint256, uint256, uint256, uint256) { + bool withFee = _feeStrategy != address(0); + // pick the highest GHO amount possible for given asset amount + uint256 grossAmount = IGsmPriceStrategy(PRICE_STRATEGY).getAssetPriceInGho(assetAmount, true); + uint256 fee = withFee ? IGsmFeeStrategy(_feeStrategy).getBuyFee(grossAmount) : 0; + uint256 ghoSold = grossAmount + fee; + uint256 finalGrossAmount = withFee + ? IGsmFeeStrategy(_feeStrategy).getGrossAmountFromTotalBought(ghoSold) + : ghoSold; + // pick the lowest asset amount possible for given GHO amount + uint256 finalAssetAmount = IGsmPriceStrategy(PRICE_STRATEGY).getGhoPriceInAsset( + finalGrossAmount, + false + ); + uint256 finalFee = ghoSold - finalGrossAmount; + return (finalAssetAmount, finalGrossAmount + finalFee, finalGrossAmount, finalFee); + } + + /** + * @dev Returns the amount of GHO bought in exchange of a given amount of underlying asset + * @param assetAmount The amount of underlying asset to sell + * @return The exact amount of asset the user sells + * @return The total amount of GHO the user buys (gross amount in GHO minus fee) + * @return The gross amount of GHO + * @return The fee amount in GHO, applied to the gross amount of GHO + */ + function _calculateGhoAmountForSellAsset( + uint256 assetAmount + ) internal view returns (uint256, uint256, uint256, uint256) { + bool withFee = _feeStrategy != address(0); + // pick the lowest GHO amount possible for given asset amount + uint256 grossAmount = IGsmPriceStrategy(PRICE_STRATEGY).getAssetPriceInGho(assetAmount, false); + uint256 fee = withFee ? IGsmFeeStrategy(_feeStrategy).getSellFee(grossAmount) : 0; + uint256 ghoBought = grossAmount - fee; + uint256 finalGrossAmount = withFee + ? IGsmFeeStrategy(_feeStrategy).getGrossAmountFromTotalSold(ghoBought) + : ghoBought; + // pick the highest asset amount possible for given GHO amount + uint256 finalAssetAmount = IGsmPriceStrategy(PRICE_STRATEGY).getGhoPriceInAsset( + finalGrossAmount, + true + ); + uint256 finalFee = finalGrossAmount - ghoBought; + return (finalAssetAmount, finalGrossAmount - finalFee, finalGrossAmount, finalFee); + } + + /** + * @dev Updates Fee Strategy + * @param feeStrategy The address of the new Fee Strategy + */ + function _updateFeeStrategy(address feeStrategy) internal { + address oldFeeStrategy = _feeStrategy; + _feeStrategy = feeStrategy; + emit FeeStrategyUpdated(oldFeeStrategy, feeStrategy); + } + + /** + * @dev Updates Exposure Cap + * @param exposureCap The value of the new Exposure Cap + */ + function _updateExposureCap(uint128 exposureCap) internal { + uint128 oldExposureCap = _exposureCap; + _exposureCap = exposureCap; + emit ExposureCapUpdated(oldExposureCap, exposureCap); + } + + /** + * @dev Updates GHO Treasury Address + * @param newGhoTreasury The address of the new GHO Treasury + */ + function _updateGhoTreasury(address newGhoTreasury) internal { + require(newGhoTreasury != address(0), 'ZERO_ADDRESS_NOT_VALID'); + address oldGhoTreasury = _ghoTreasury; + _ghoTreasury = newGhoTreasury; + emit GhoTreasuryUpdated(oldGhoTreasury, newGhoTreasury); + } + + /// @inheritdoc VersionedInitializable + function getRevision() internal pure virtual override returns (uint256) { + return GSM_REVISION(); + } +} diff --git a/certora/GSM/mutations/mutants/Gsm/Gsm.sol1 copy.sol b/certora/GSM/mutations/mutants/Gsm/Gsm.sol1 copy.sol new file mode 100644 index 00000000..dbf4aa90 --- /dev/null +++ b/certora/GSM/mutations/mutants/Gsm/Gsm.sol1 copy.sol @@ -0,0 +1,561 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.10; + +import {VersionedInitializable} from '@aave/core-v3/contracts/protocol/libraries/aave-upgradeability/VersionedInitializable.sol'; +import {IERC20} from '@aave/core-v3/contracts/dependencies/openzeppelin/contracts/IERC20.sol'; +import {GPv2SafeERC20} from '@aave/core-v3/contracts/dependencies/gnosis/contracts/GPv2SafeERC20.sol'; +import {EIP712} from '@openzeppelin/contracts/utils/cryptography/EIP712.sol'; +import {SignatureChecker} from '@openzeppelin/contracts/utils/cryptography/SignatureChecker.sol'; +import {SafeCast} from '@openzeppelin/contracts/utils/math/SafeCast.sol'; +import {AccessControl} from '@openzeppelin/contracts/access/AccessControl.sol'; +import {IGhoFacilitator} from '../../gho/interfaces/IGhoFacilitator.sol'; +import {IGhoToken} from '../../gho/interfaces/IGhoToken.sol'; +import {IGsmPriceStrategy} from './priceStrategy/interfaces/IGsmPriceStrategy.sol'; +import {IGsmFeeStrategy} from './feeStrategy/interfaces/IGsmFeeStrategy.sol'; +import {IGsm} from './interfaces/IGsm.sol'; + +/** + * @title Gsm + * @author Aave + * @notice GHO Stability Module. It provides buy/sell facilities to go to/from an underlying asset to/from GHO. + * @dev To be covered by a proxy contract. + */ +contract Gsm is AccessControl, VersionedInitializable, EIP712, IGsm { + using GPv2SafeERC20 for IERC20; + using SafeCast for uint256; + + /// @inheritdoc IGsm + bytes32 public constant CONFIGURATOR_ROLE = keccak256('CONFIGURATOR_ROLE'); + + /// @inheritdoc IGsm + bytes32 public constant TOKEN_RESCUER_ROLE = keccak256('TOKEN_RESCUER_ROLE'); + + /// @inheritdoc IGsm + bytes32 public constant SWAP_FREEZER_ROLE = keccak256('SWAP_FREEZER_ROLE'); + + /// @inheritdoc IGsm + bytes32 public constant LIQUIDATOR_ROLE = keccak256('LIQUIDATOR_ROLE'); + + /// @inheritdoc IGsm + bytes32 public constant BUY_ASSET_WITH_SIG_TYPEHASH = + keccak256( + 'BuyAssetWithSig(address originator,uint256 minAmount,address receiver,uint256 nonce,uint256 deadline)' + ); + + /// @inheritdoc IGsm + bytes32 public constant SELL_ASSET_WITH_SIG_TYPEHASH = + keccak256( + 'SellAssetWithSig(address originator,uint256 maxAmount,address receiver,uint256 nonce,uint256 deadline)' + ); + + /// @inheritdoc IGsm + address public immutable GHO_TOKEN; + + /// @inheritdoc IGsm + address public immutable UNDERLYING_ASSET; + + /// @inheritdoc IGsm + address public immutable PRICE_STRATEGY; + + /// @inheritdoc IGsm + mapping(address => uint256) public nonces; + + address internal _ghoTreasury; + address internal _feeStrategy; + bool internal _isFrozen; + bool internal _isSeized; + uint128 internal _exposureCap; + uint128 internal _currentExposure; + uint128 internal _accruedFees; + + /** + * @dev Require GSM to not be frozen for functions marked by this modifier + */ + modifier notFrozen() { + require(!_isFrozen, 'GSM_FROZEN'); + _; + } + + /** + * @dev Require GSM to not be seized for functions marked by this modifier + */ + modifier notSeized() { + require(!_isSeized, 'GSM_SEIZED'); + _; + } + + /** + * @dev Constructor + * @param ghoToken The address of the GHO token contract + * @param underlyingAsset The address of the collateral asset + * @param priceStrategy The address of the price strategy + */ + constructor(address ghoToken, address underlyingAsset, address priceStrategy) EIP712('GSM', '1') { + require(ghoToken != address(0), 'ZERO_ADDRESS_NOT_VALID'); + require(underlyingAsset != address(0), 'ZERO_ADDRESS_NOT_VALID'); + require( + IGsmPriceStrategy(priceStrategy).UNDERLYING_ASSET() == underlyingAsset, + 'INVALID_PRICE_STRATEGY' + ); + GHO_TOKEN = ghoToken; + UNDERLYING_ASSET = underlyingAsset; + PRICE_STRATEGY = priceStrategy; + } + + /** + * @notice GSM initializer + * @param admin The address of the default admin role + * @param ghoTreasury The address of the GHO treasury + * @param exposureCap Maximum amount of user-supplied underlying asset in GSM + */ + function initialize( + address admin, + address ghoTreasury, + uint128 exposureCap + ) external initializer { + require(admin != address(0), 'ZERO_ADDRESS_NOT_VALID'); + _grantRole(DEFAULT_ADMIN_ROLE, admin); + /// FunctionCallMutation of: _grantRole(CONFIGURATOR_ROLE, admin); + admin; + _updateGhoTreasury(ghoTreasury); + _updateExposureCap(exposureCap); + } + + /// @inheritdoc IGsm + function buyAsset( + uint256 minAmount, + address receiver + ) external notFrozen notSeized returns (uint256, uint256) { + return _buyAsset(msg.sender, minAmount, receiver); + } + + /// @inheritdoc IGsm + function buyAssetWithSig( + address originator, + uint256 minAmount, + address receiver, + uint256 deadline, + bytes calldata signature + ) external notFrozen notSeized returns (uint256, uint256) { + require(deadline >= block.timestamp, 'SIGNATURE_DEADLINE_EXPIRED'); + bytes32 digest = keccak256( + abi.encode( + '\x19\x01', + _domainSeparatorV4(), + BUY_ASSET_WITH_SIG_TYPEHASH, + abi.encode(originator, minAmount, receiver, nonces[originator]++, deadline) + ) + ); + require( + SignatureChecker.isValidSignatureNow(originator, digest, signature), + 'SIGNATURE_INVALID' + ); + + return _buyAsset(originator, minAmount, receiver); + } + + /// @inheritdoc IGsm + function sellAsset( + uint256 maxAmount, + address receiver + ) external notFrozen notSeized returns (uint256, uint256) { + return _sellAsset(msg.sender, maxAmount, receiver); + } + + /// @inheritdoc IGsm + function sellAssetWithSig( + address originator, + uint256 maxAmount, + address receiver, + uint256 deadline, + bytes calldata signature + ) external notFrozen notSeized returns (uint256, uint256) { + require(deadline >= block.timestamp, 'SIGNATURE_DEADLINE_EXPIRED'); + bytes32 digest = keccak256( + abi.encode( + '\x19\x01', + _domainSeparatorV4(), + SELL_ASSET_WITH_SIG_TYPEHASH, + abi.encode(originator, maxAmount, receiver, nonces[originator]++, deadline) + ) + ); + require( + SignatureChecker.isValidSignatureNow(originator, digest, signature), + 'SIGNATURE_INVALID' + ); + + return _sellAsset(originator, maxAmount, receiver); + } + + /// @inheritdoc IGsm + function rescueTokens( + address token, + address to, + uint256 amount + ) external onlyRole(TOKEN_RESCUER_ROLE) { + require(amount > 0, 'INVALID_AMOUNT'); + if (token == GHO_TOKEN) { + uint256 rescuableBalance = IERC20(token).balanceOf(address(this)) - _accruedFees; + require(rescuableBalance >= amount, 'INSUFFICIENT_GHO_TO_RESCUE'); + } + if (token == UNDERLYING_ASSET) { + uint256 rescuableBalance = IERC20(token).balanceOf(address(this)) - _currentExposure; + require(rescuableBalance >= amount, 'INSUFFICIENT_EXOGENOUS_ASSET_TO_RESCUE'); + } + IERC20(token).safeTransfer(to, amount); + emit TokensRescued(token, to, amount); + } + + /// @inheritdoc IGsm + function setSwapFreeze(bool enable) external onlyRole(SWAP_FREEZER_ROLE) { + if (enable) { + require(!_isFrozen, 'GSM_ALREADY_FROZEN'); + } else { + require(_isFrozen, 'GSM_ALREADY_UNFROZEN'); + } + _isFrozen = enable; + emit SwapFreeze(msg.sender, enable); + } + + /// @inheritdoc IGsm + function seize() external notSeized onlyRole(LIQUIDATOR_ROLE) returns (uint256) { + _isSeized = true; + _currentExposure = 0; + _updateExposureCap(0); + + (, uint256 ghoMinted) = IGhoToken(GHO_TOKEN).getFacilitatorBucket(address(this)); + uint256 underlyingBalance = IERC20(UNDERLYING_ASSET).balanceOf(address(this)); + if (underlyingBalance > 0) { + IERC20(UNDERLYING_ASSET).safeTransfer(_ghoTreasury, underlyingBalance); + } + + emit Seized(msg.sender, _ghoTreasury, underlyingBalance, ghoMinted); + return underlyingBalance; + } + + /// @inheritdoc IGsm + function burnAfterSeize(uint256 amount) external onlyRole(LIQUIDATOR_ROLE) returns (uint256) { + require(_isSeized, 'GSM_NOT_SEIZED'); + require(amount > 0, 'INVALID_AMOUNT'); + + (, uint256 ghoMinted) = IGhoToken(GHO_TOKEN).getFacilitatorBucket(address(this)); + if (amount > ghoMinted) { + amount = ghoMinted; + } + IGhoToken(GHO_TOKEN).transferFrom(msg.sender, address(this), amount); + IGhoToken(GHO_TOKEN).burn(amount); + + emit BurnAfterSeize(msg.sender, amount, (ghoMinted - amount)); + return amount; + } + + /// @inheritdoc IGsm + function updateFeeStrategy(address feeStrategy) external onlyRole(CONFIGURATOR_ROLE) { + _updateFeeStrategy(feeStrategy); + } + + /// @inheritdoc IGsm + function updateExposureCap(uint128 exposureCap) external onlyRole(CONFIGURATOR_ROLE) { + _updateExposureCap(exposureCap); + } + + /// @inheritdoc IGhoFacilitator + function distributeFeesToTreasury() public virtual override { + uint256 accruedFees = _accruedFees; + if (accruedFees > 0) { + _accruedFees = 0; + IERC20(GHO_TOKEN).transfer(_ghoTreasury, accruedFees); + emit FeesDistributedToTreasury(_ghoTreasury, GHO_TOKEN, accruedFees); + } + } + + /// @inheritdoc IGhoFacilitator + function updateGhoTreasury(address newGhoTreasury) external override onlyRole(CONFIGURATOR_ROLE) { + _updateGhoTreasury(newGhoTreasury); + } + + /// @inheritdoc IGsm + function DOMAIN_SEPARATOR() external view returns (bytes32) { + return _domainSeparatorV4(); + } + + /// @inheritdoc IGsm + function getGhoAmountForBuyAsset( + uint256 minAssetAmount + ) external view returns (uint256, uint256, uint256, uint256) { + return _calculateGhoAmountForBuyAsset(minAssetAmount); + } + + /// @inheritdoc IGsm + function getGhoAmountForSellAsset( + uint256 maxAssetAmount + ) external view returns (uint256, uint256, uint256, uint256) { + return _calculateGhoAmountForSellAsset(maxAssetAmount); + } + + /// @inheritdoc IGsm + function getAssetAmountForBuyAsset( + uint256 maxGhoAmount + ) external view returns (uint256, uint256, uint256, uint256) { + bool withFee = _feeStrategy != address(0); + uint256 grossAmount = withFee + ? IGsmFeeStrategy(_feeStrategy).getGrossAmountFromTotalBought(maxGhoAmount) + : maxGhoAmount; + // round down so maxGhoAmount is guaranteed + uint256 assetAmount = IGsmPriceStrategy(PRICE_STRATEGY).getGhoPriceInAsset(grossAmount, false); + uint256 finalGrossAmount = IGsmPriceStrategy(PRICE_STRATEGY).getAssetPriceInGho( + assetAmount, + true // TODO + ); + uint256 finalFee = withFee ? IGsmFeeStrategy(_feeStrategy).getBuyFee(finalGrossAmount) : 0; + return (assetAmount, finalGrossAmount + finalFee, finalGrossAmount, finalFee); + } + + /// @inheritdoc IGsm + function getAssetAmountForSellAsset( + uint256 minGhoAmount + ) external view returns (uint256, uint256, uint256, uint256) { + bool withFee = _feeStrategy != address(0); + uint256 grossAmount = withFee + ? IGsmFeeStrategy(_feeStrategy).getGrossAmountFromTotalSold(minGhoAmount) + : minGhoAmount; + // round up so minGhoAmount is guaranteed + uint256 assetAmount = IGsmPriceStrategy(PRICE_STRATEGY).getGhoPriceInAsset(grossAmount, true); + uint256 finalGrossAmount = IGsmPriceStrategy(PRICE_STRATEGY).getAssetPriceInGho( + assetAmount, + false // TODO + ); + uint256 finalFee = withFee ? IGsmFeeStrategy(_feeStrategy).getSellFee(finalGrossAmount) : 0; + return (assetAmount, finalGrossAmount - finalFee, finalGrossAmount, finalFee); + } + + /// @inheritdoc IGsm + function getAvailableUnderlyingExposure() external view returns (uint256) { + return _exposureCap > _currentExposure ? _exposureCap - _currentExposure : 0; + } + + /// @inheritdoc IGsm + function getAvailableLiquidity() external view returns (uint256) { + return _currentExposure; + } + + /// @inheritdoc IGsm + function getFeeStrategy() external view returns (address) { + return _feeStrategy; + } + + /// @inheritdoc IGsm + function getAccruedFees() external view returns (uint256) { + return _accruedFees; + } + + /// @inheritdoc IGsm + function getIsFrozen() external view returns (bool) { + return _isFrozen; + } + + /// @inheritdoc IGsm + function getIsSeized() external view returns (bool) { + return _isSeized; + } + + /// @inheritdoc IGsm + function canSwap() external view returns (bool) { + return !_isFrozen && !_isSeized; + } + + /// @inheritdoc IGhoFacilitator + function getGhoTreasury() external view override returns (address) { + return _ghoTreasury; + } + + /// @inheritdoc IGsm + function GSM_REVISION() public pure virtual override returns (uint256) { + return 1; + } + + /** + * @dev Buys an underlying asset with GHO + * @param originator The originator of the request + * @param minAmount The minimum amount of the underlying asset desired for purchase + * @param receiver The recipient address of the underlying asset being purchased + * @return The amount of underlying asset bought + * @return The amount of GHO sold by the user + */ + function _buyAsset( + address originator, + uint256 minAmount, + address receiver + ) internal returns (uint256, uint256) { + ( + uint256 assetAmount, + uint256 ghoSold, + uint256 grossAmount, + uint256 fee + ) = _calculateGhoAmountForBuyAsset(minAmount); + + _beforeBuyAsset(originator, assetAmount, receiver); + + require(assetAmount > 0, 'INVALID_AMOUNT'); + require(_currentExposure >= assetAmount, 'INSUFFICIENT_AVAILABLE_EXOGENOUS_ASSET_LIQUIDITY'); + + _currentExposure -= uint128(assetAmount); + _accruedFees += fee.toUint128(); + IGhoToken(GHO_TOKEN).transferFrom(originator, address(this), ghoSold); + IGhoToken(GHO_TOKEN).burn(grossAmount); + IERC20(UNDERLYING_ASSET).safeTransfer(receiver, assetAmount); + + emit BuyAsset(originator, receiver, assetAmount, ghoSold, fee); + return (assetAmount, ghoSold); + } + + /** + * @dev Hook that is called before `buyAsset`. + * @dev This can be used to add custom logic + * @param originator Originator of the request + * @param amount The amount of the underlying asset desired for purchase + * @param receiver Recipient address of the underlying asset being purchased + */ + function _beforeBuyAsset(address originator, uint256 amount, address receiver) internal virtual {} + + /** + * @dev Sells an underlying asset for GHO + * @param originator The originator of the request + * @param maxAmount The maximum amount of the underlying asset desired to sell + * @param receiver The recipient address of the GHO being purchased + * @return The amount of underlying asset sold + * @return The amount of GHO bought by the user + */ + function _sellAsset( + address originator, + uint256 maxAmount, + address receiver + ) internal returns (uint256, uint256) { + ( + uint256 assetAmount, + uint256 ghoBought, + uint256 grossAmount, + uint256 fee + ) = _calculateGhoAmountForSellAsset(maxAmount); + + _beforeSellAsset(originator, assetAmount, receiver); + + require(assetAmount > 0, 'INVALID_AMOUNT'); + require(_currentExposure + assetAmount <= _exposureCap, 'EXOGENOUS_ASSET_EXPOSURE_TOO_HIGH'); + + _currentExposure += uint128(assetAmount); + _accruedFees += fee.toUint128(); + IERC20(UNDERLYING_ASSET).safeTransferFrom(originator, address(this), assetAmount); + + IGhoToken(GHO_TOKEN).mint(address(this), grossAmount); + IGhoToken(GHO_TOKEN).transfer(receiver, ghoBought); + + emit SellAsset(originator, receiver, assetAmount, grossAmount, fee); + return (assetAmount, ghoBought); + } + + /** + * @dev Hook that is called before `sellAsset`. + * @dev This can be used to add custom logic + * @param originator Originator of the request + * @param amount The amount of the underlying asset desired to sell + * @param receiver Recipient address of the GHO being purchased + */ + function _beforeSellAsset( + address originator, + uint256 amount, + address receiver + ) internal virtual {} + + /** + * @dev Returns the amount of GHO sold in exchange of buying underlying asset + * @param assetAmount The amount of underlying asset to buy + * @return The exact amount of asset the user purchases + * @return The total amount of GHO the user sells (gross amount in GHO plus fee) + * @return The gross amount of GHO + * @return The fee amount in GHO, applied on top of gross amount of GHO + */ + function _calculateGhoAmountForBuyAsset( + uint256 assetAmount + ) internal view returns (uint256, uint256, uint256, uint256) { + bool withFee = _feeStrategy != address(0); + // pick the highest GHO amount possible for given asset amount + uint256 grossAmount = IGsmPriceStrategy(PRICE_STRATEGY).getAssetPriceInGho(assetAmount, true); + uint256 fee = withFee ? IGsmFeeStrategy(_feeStrategy).getBuyFee(grossAmount) : 0; + uint256 ghoSold = grossAmount + fee; + uint256 finalGrossAmount = withFee + ? IGsmFeeStrategy(_feeStrategy).getGrossAmountFromTotalBought(ghoSold) + : ghoSold; + // pick the lowest asset amount possible for given GHO amount + uint256 finalAssetAmount = IGsmPriceStrategy(PRICE_STRATEGY).getGhoPriceInAsset( + finalGrossAmount, + false + ); + uint256 finalFee = ghoSold - finalGrossAmount; + return (finalAssetAmount, finalGrossAmount + finalFee, finalGrossAmount, finalFee); + } + + /** + * @dev Returns the amount of GHO bought in exchange of a given amount of underlying asset + * @param assetAmount The amount of underlying asset to sell + * @return The exact amount of asset the user sells + * @return The total amount of GHO the user buys (gross amount in GHO minus fee) + * @return The gross amount of GHO + * @return The fee amount in GHO, applied to the gross amount of GHO + */ + function _calculateGhoAmountForSellAsset( + uint256 assetAmount + ) internal view returns (uint256, uint256, uint256, uint256) { + bool withFee = _feeStrategy != address(0); + // pick the lowest GHO amount possible for given asset amount + uint256 grossAmount = IGsmPriceStrategy(PRICE_STRATEGY).getAssetPriceInGho(assetAmount, false); + uint256 fee = withFee ? IGsmFeeStrategy(_feeStrategy).getSellFee(grossAmount) : 0; + uint256 ghoBought = grossAmount - fee; + uint256 finalGrossAmount = withFee + ? IGsmFeeStrategy(_feeStrategy).getGrossAmountFromTotalSold(ghoBought) + : ghoBought; + // pick the highest asset amount possible for given GHO amount + uint256 finalAssetAmount = IGsmPriceStrategy(PRICE_STRATEGY).getGhoPriceInAsset( + finalGrossAmount, + true + ); + uint256 finalFee = finalGrossAmount - ghoBought; + return (finalAssetAmount, finalGrossAmount - finalFee, finalGrossAmount, finalFee); + } + + /** + * @dev Updates Fee Strategy + * @param feeStrategy The address of the new Fee Strategy + */ + function _updateFeeStrategy(address feeStrategy) internal { + address oldFeeStrategy = _feeStrategy; + _feeStrategy = feeStrategy; + emit FeeStrategyUpdated(oldFeeStrategy, feeStrategy); + } + + /** + * @dev Updates Exposure Cap + * @param exposureCap The value of the new Exposure Cap + */ + function _updateExposureCap(uint128 exposureCap) internal { + uint128 oldExposureCap = _exposureCap; + _exposureCap = exposureCap; + emit ExposureCapUpdated(oldExposureCap, exposureCap); + } + + /** + * @dev Updates GHO Treasury Address + * @param newGhoTreasury The address of the new GHO Treasury + */ + function _updateGhoTreasury(address newGhoTreasury) internal { + require(newGhoTreasury != address(0), 'ZERO_ADDRESS_NOT_VALID'); + address oldGhoTreasury = _ghoTreasury; + _ghoTreasury = newGhoTreasury; + emit GhoTreasuryUpdated(oldGhoTreasury, newGhoTreasury); + } + + /// @inheritdoc VersionedInitializable + function getRevision() internal pure virtual override returns (uint256) { + return GSM_REVISION(); + } +} diff --git a/certora/GSM/mutations/mutants/Gsm/Gsm.sol1.sol b/certora/GSM/mutations/mutants/Gsm/Gsm.sol1.sol new file mode 100644 index 00000000..b64bc5cb --- /dev/null +++ b/certora/GSM/mutations/mutants/Gsm/Gsm.sol1.sol @@ -0,0 +1,561 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.10; + +import {VersionedInitializable} from '@aave/core-v3/contracts/protocol/libraries/aave-upgradeability/VersionedInitializable.sol'; +import {IERC20} from '@aave/core-v3/contracts/dependencies/openzeppelin/contracts/IERC20.sol'; +import {GPv2SafeERC20} from '@aave/core-v3/contracts/dependencies/gnosis/contracts/GPv2SafeERC20.sol'; +import {EIP712} from '@openzeppelin/contracts/utils/cryptography/EIP712.sol'; +import {SignatureChecker} from '@openzeppelin/contracts/utils/cryptography/SignatureChecker.sol'; +import {SafeCast} from '@openzeppelin/contracts/utils/math/SafeCast.sol'; +import {AccessControl} from '@openzeppelin/contracts/access/AccessControl.sol'; +import {IGhoFacilitator} from '../../gho/interfaces/IGhoFacilitator.sol'; +import {IGhoToken} from '../../gho/interfaces/IGhoToken.sol'; +import {IGsmPriceStrategy} from './priceStrategy/interfaces/IGsmPriceStrategy.sol'; +import {IGsmFeeStrategy} from './feeStrategy/interfaces/IGsmFeeStrategy.sol'; +import {IGsm} from './interfaces/IGsm.sol'; + +/** + * @title Gsm + * @author Aave + * @notice GHO Stability Module. It provides buy/sell facilities to go to/from an underlying asset to/from GHO. + * @dev To be covered by a proxy contract. + */ +contract Gsm is AccessControl, VersionedInitializable, EIP712, IGsm { + using GPv2SafeERC20 for IERC20; + using SafeCast for uint256; + + /// @inheritdoc IGsm + bytes32 public constant CONFIGURATOR_ROLE = keccak256('CONFIGURATOR_ROLE'); + + /// @inheritdoc IGsm + bytes32 public constant TOKEN_RESCUER_ROLE = keccak256('TOKEN_RESCUER_ROLE'); + + /// @inheritdoc IGsm + bytes32 public constant SWAP_FREEZER_ROLE = keccak256('SWAP_FREEZER_ROLE'); + + /// @inheritdoc IGsm + bytes32 public constant LIQUIDATOR_ROLE = keccak256('LIQUIDATOR_ROLE'); + + /// @inheritdoc IGsm + bytes32 public constant BUY_ASSET_WITH_SIG_TYPEHASH = + keccak256( + 'BuyAssetWithSig(address originator,uint256 minAmount,address receiver,uint256 nonce,uint256 deadline)' + ); + + /// @inheritdoc IGsm + bytes32 public constant SELL_ASSET_WITH_SIG_TYPEHASH = + keccak256( + 'SellAssetWithSig(address originator,uint256 maxAmount,address receiver,uint256 nonce,uint256 deadline)' + ); + + /// @inheritdoc IGsm + address public immutable GHO_TOKEN; + + /// @inheritdoc IGsm + address public immutable UNDERLYING_ASSET; + + /// @inheritdoc IGsm + address public immutable PRICE_STRATEGY; + + /// @inheritdoc IGsm + mapping(address => uint256) public nonces; + + address internal _ghoTreasury; + address internal _feeStrategy; + bool internal _isFrozen; + bool internal _isSeized; + uint128 internal _exposureCap; + uint128 internal _currentExposure; + uint128 internal _accruedFees; + + /** + * @dev Require GSM to not be frozen for functions marked by this modifier + */ + modifier notFrozen() { + require(!_isFrozen, 'GSM_FROZEN'); + _; + } + + /** + * @dev Require GSM to not be seized for functions marked by this modifier + */ + modifier notSeized() { + require(!_isSeized, 'GSM_SEIZED'); + _; + } + + /** + * @dev Constructor + * @param ghoToken The address of the GHO token contract + * @param underlyingAsset The address of the collateral asset + * @param priceStrategy The address of the price strategy + */ + constructor(address ghoToken, address underlyingAsset, address priceStrategy) EIP712('GSM', '1') { + require(ghoToken != address(0), 'ZERO_ADDRESS_NOT_VALID'); + require(underlyingAsset != address(0), 'ZERO_ADDRESS_NOT_VALID'); + require( + IGsmPriceStrategy(priceStrategy).UNDERLYING_ASSET() == underlyingAsset, + 'INVALID_PRICE_STRATEGY' + ); + GHO_TOKEN = ghoToken; + UNDERLYING_ASSET = underlyingAsset; + PRICE_STRATEGY = priceStrategy; + } + + /** + * @notice GSM initializer + * @param admin The address of the default admin role + * @param ghoTreasury The address of the GHO treasury + * @param exposureCap Maximum amount of user-supplied underlying asset in GSM + */ + function initialize( + address admin, + address ghoTreasury, + uint128 exposureCap + ) external initializer { + require(admin != address(0), 'ZERO_ADDRESS_NOT_VALID'); + _grantRole(DEFAULT_ADMIN_ROLE, admin); + _grantRole(CONFIGURATOR_ROLE, admin); + _updateGhoTreasury(ghoTreasury); + _updateExposureCap(exposureCap); + } + + /// @inheritdoc IGsm + function buyAsset( + uint256 minAmount, + address receiver + ) external notFrozen notSeized returns (uint256, uint256) { + return _buyAsset(msg.sender, minAmount, receiver); + } + + /// @inheritdoc IGsm + function buyAssetWithSig( + address originator, + uint256 minAmount, + address receiver, + uint256 deadline, + bytes calldata signature + ) external notFrozen notSeized returns (uint256, uint256) { + require(deadline >= block.timestamp, 'SIGNATURE_DEADLINE_EXPIRED'); + bytes32 digest = keccak256( + abi.encode( + '\x19\x01', + _domainSeparatorV4(), + BUY_ASSET_WITH_SIG_TYPEHASH, + abi.encode(originator, minAmount, receiver, nonces[originator]++, deadline) + ) + ); + require( + SignatureChecker.isValidSignatureNow(originator, digest, signature), + 'SIGNATURE_INVALID' + ); + + return _buyAsset(originator, minAmount, receiver); + } + + /// @inheritdoc IGsm + function sellAsset( + uint256 maxAmount, + address receiver + ) external notFrozen notSeized returns (uint256, uint256) { + return _sellAsset(msg.sender, maxAmount, receiver); + } + + /// @inheritdoc IGsm + function sellAssetWithSig( + address originator, + uint256 maxAmount, + address receiver, + uint256 deadline, + bytes calldata signature + ) external notFrozen notSeized returns (uint256, uint256) { + require(deadline >= block.timestamp, 'SIGNATURE_DEADLINE_EXPIRED'); + bytes32 digest = keccak256( + abi.encode( + '\x19\x01', + _domainSeparatorV4(), + SELL_ASSET_WITH_SIG_TYPEHASH, + abi.encode(originator, maxAmount, receiver, nonces[originator]++, deadline) + ) + ); + require( + SignatureChecker.isValidSignatureNow(originator, digest, signature), + 'SIGNATURE_INVALID' + ); + + return _sellAsset(originator, maxAmount, receiver); + } + + /// @inheritdoc IGsm + function rescueTokens( + address token, + address to, + uint256 amount + ) external onlyRole(TOKEN_RESCUER_ROLE) { + require(amount > 0, 'INVALID_AMOUNT'); + if (token == GHO_TOKEN) { + uint256 rescuableBalance = IERC20(token).balanceOf(address(this)) - _accruedFees; + require(rescuableBalance >= amount, 'INSUFFICIENT_GHO_TO_RESCUE'); + } + if (token == UNDERLYING_ASSET) { + uint256 rescuableBalance = IERC20(token).balanceOf(address(this)) - _currentExposure; + require(rescuableBalance >= amount, 'INSUFFICIENT_EXOGENOUS_ASSET_TO_RESCUE'); + } + IERC20(token).safeTransfer(to, amount); + emit TokensRescued(token, to, amount); + } + + /// @inheritdoc IGsm + function setSwapFreeze(bool enable) external onlyRole(SWAP_FREEZER_ROLE) { + if (enable) { + /// RequireMutation of: require(!_isFrozen, 'GSM_ALREADY_FROZEN'); + require(!(!_isFrozen), 'GSM_ALREADY_FROZEN'); + } else { + require(_isFrozen, 'GSM_ALREADY_UNFROZEN'); + } + _isFrozen = enable; + emit SwapFreeze(msg.sender, enable); + } + + /// @inheritdoc IGsm + function seize() external notSeized onlyRole(LIQUIDATOR_ROLE) returns (uint256) { + _isSeized = true; + _currentExposure = 0; + _updateExposureCap(0); + + (, uint256 ghoMinted) = IGhoToken(GHO_TOKEN).getFacilitatorBucket(address(this)); + uint256 underlyingBalance = IERC20(UNDERLYING_ASSET).balanceOf(address(this)); + if (underlyingBalance > 0) { + IERC20(UNDERLYING_ASSET).safeTransfer(_ghoTreasury, underlyingBalance); + } + + emit Seized(msg.sender, _ghoTreasury, underlyingBalance, ghoMinted); + return underlyingBalance; + } + + /// @inheritdoc IGsm + function burnAfterSeize(uint256 amount) external onlyRole(LIQUIDATOR_ROLE) returns (uint256) { + require(_isSeized, 'GSM_NOT_SEIZED'); + require(amount > 0, 'INVALID_AMOUNT'); + + (, uint256 ghoMinted) = IGhoToken(GHO_TOKEN).getFacilitatorBucket(address(this)); + if (amount > ghoMinted) { + amount = ghoMinted; + } + IGhoToken(GHO_TOKEN).transferFrom(msg.sender, address(this), amount); + IGhoToken(GHO_TOKEN).burn(amount); + + emit BurnAfterSeize(msg.sender, amount, (ghoMinted - amount)); + return amount; + } + + /// @inheritdoc IGsm + function updateFeeStrategy(address feeStrategy) external onlyRole(CONFIGURATOR_ROLE) { + _updateFeeStrategy(feeStrategy); + } + + /// @inheritdoc IGsm + function updateExposureCap(uint128 exposureCap) external onlyRole(CONFIGURATOR_ROLE) { + _updateExposureCap(exposureCap); + } + + /// @inheritdoc IGhoFacilitator + function distributeFeesToTreasury() public virtual override { + uint256 accruedFees = _accruedFees; + if (accruedFees > 0) { + _accruedFees = 0; + IERC20(GHO_TOKEN).transfer(_ghoTreasury, accruedFees); + emit FeesDistributedToTreasury(_ghoTreasury, GHO_TOKEN, accruedFees); + } + } + + /// @inheritdoc IGhoFacilitator + function updateGhoTreasury(address newGhoTreasury) external override onlyRole(CONFIGURATOR_ROLE) { + _updateGhoTreasury(newGhoTreasury); + } + + /// @inheritdoc IGsm + function DOMAIN_SEPARATOR() external view returns (bytes32) { + return _domainSeparatorV4(); + } + + /// @inheritdoc IGsm + function getGhoAmountForBuyAsset( + uint256 minAssetAmount + ) external view returns (uint256, uint256, uint256, uint256) { + return _calculateGhoAmountForBuyAsset(minAssetAmount); + } + + /// @inheritdoc IGsm + function getGhoAmountForSellAsset( + uint256 maxAssetAmount + ) external view returns (uint256, uint256, uint256, uint256) { + return _calculateGhoAmountForSellAsset(maxAssetAmount); + } + + /// @inheritdoc IGsm + function getAssetAmountForBuyAsset( + uint256 maxGhoAmount + ) external view returns (uint256, uint256, uint256, uint256) { + bool withFee = _feeStrategy != address(0); + uint256 grossAmount = withFee + ? IGsmFeeStrategy(_feeStrategy).getGrossAmountFromTotalBought(maxGhoAmount) + : maxGhoAmount; + // round down so maxGhoAmount is guaranteed + uint256 assetAmount = IGsmPriceStrategy(PRICE_STRATEGY).getGhoPriceInAsset(grossAmount, false); + uint256 finalGrossAmount = IGsmPriceStrategy(PRICE_STRATEGY).getAssetPriceInGho( + assetAmount, + true // TODO + ); + uint256 finalFee = withFee ? IGsmFeeStrategy(_feeStrategy).getBuyFee(finalGrossAmount) : 0; + return (assetAmount, finalGrossAmount + finalFee, finalGrossAmount, finalFee); + } + + /// @inheritdoc IGsm + function getAssetAmountForSellAsset( + uint256 minGhoAmount + ) external view returns (uint256, uint256, uint256, uint256) { + bool withFee = _feeStrategy != address(0); + uint256 grossAmount = withFee + ? IGsmFeeStrategy(_feeStrategy).getGrossAmountFromTotalSold(minGhoAmount) + : minGhoAmount; + // round up so minGhoAmount is guaranteed + uint256 assetAmount = IGsmPriceStrategy(PRICE_STRATEGY).getGhoPriceInAsset(grossAmount, true); + uint256 finalGrossAmount = IGsmPriceStrategy(PRICE_STRATEGY).getAssetPriceInGho( + assetAmount, + false // TODO + ); + uint256 finalFee = withFee ? IGsmFeeStrategy(_feeStrategy).getSellFee(finalGrossAmount) : 0; + return (assetAmount, finalGrossAmount - finalFee, finalGrossAmount, finalFee); + } + + /// @inheritdoc IGsm + function getAvailableUnderlyingExposure() external view returns (uint256) { + return _exposureCap > _currentExposure ? _exposureCap - _currentExposure : 0; + } + + /// @inheritdoc IGsm + function getAvailableLiquidity() external view returns (uint256) { + return _currentExposure; + } + + /// @inheritdoc IGsm + function getFeeStrategy() external view returns (address) { + return _feeStrategy; + } + + /// @inheritdoc IGsm + function getAccruedFees() external view returns (uint256) { + return _accruedFees; + } + + /// @inheritdoc IGsm + function getIsFrozen() external view returns (bool) { + return _isFrozen; + } + + /// @inheritdoc IGsm + function getIsSeized() external view returns (bool) { + return _isSeized; + } + + /// @inheritdoc IGsm + function canSwap() external view returns (bool) { + return !_isFrozen && !_isSeized; + } + + /// @inheritdoc IGhoFacilitator + function getGhoTreasury() external view override returns (address) { + return _ghoTreasury; + } + + /// @inheritdoc IGsm + function GSM_REVISION() public pure virtual override returns (uint256) { + return 1; + } + + /** + * @dev Buys an underlying asset with GHO + * @param originator The originator of the request + * @param minAmount The minimum amount of the underlying asset desired for purchase + * @param receiver The recipient address of the underlying asset being purchased + * @return The amount of underlying asset bought + * @return The amount of GHO sold by the user + */ + function _buyAsset( + address originator, + uint256 minAmount, + address receiver + ) internal returns (uint256, uint256) { + ( + uint256 assetAmount, + uint256 ghoSold, + uint256 grossAmount, + uint256 fee + ) = _calculateGhoAmountForBuyAsset(minAmount); + + _beforeBuyAsset(originator, assetAmount, receiver); + + require(assetAmount > 0, 'INVALID_AMOUNT'); + require(_currentExposure >= assetAmount, 'INSUFFICIENT_AVAILABLE_EXOGENOUS_ASSET_LIQUIDITY'); + + _currentExposure -= uint128(assetAmount); + _accruedFees += fee.toUint128(); + IGhoToken(GHO_TOKEN).transferFrom(originator, address(this), ghoSold); + IGhoToken(GHO_TOKEN).burn(grossAmount); + IERC20(UNDERLYING_ASSET).safeTransfer(receiver, assetAmount); + + emit BuyAsset(originator, receiver, assetAmount, ghoSold, fee); + return (assetAmount, ghoSold); + } + + /** + * @dev Hook that is called before `buyAsset`. + * @dev This can be used to add custom logic + * @param originator Originator of the request + * @param amount The amount of the underlying asset desired for purchase + * @param receiver Recipient address of the underlying asset being purchased + */ + function _beforeBuyAsset(address originator, uint256 amount, address receiver) internal virtual {} + + /** + * @dev Sells an underlying asset for GHO + * @param originator The originator of the request + * @param maxAmount The maximum amount of the underlying asset desired to sell + * @param receiver The recipient address of the GHO being purchased + * @return The amount of underlying asset sold + * @return The amount of GHO bought by the user + */ + function _sellAsset( + address originator, + uint256 maxAmount, + address receiver + ) internal returns (uint256, uint256) { + ( + uint256 assetAmount, + uint256 ghoBought, + uint256 grossAmount, + uint256 fee + ) = _calculateGhoAmountForSellAsset(maxAmount); + + _beforeSellAsset(originator, assetAmount, receiver); + + require(assetAmount > 0, 'INVALID_AMOUNT'); + require(_currentExposure + assetAmount <= _exposureCap, 'EXOGENOUS_ASSET_EXPOSURE_TOO_HIGH'); + + _currentExposure += uint128(assetAmount); + _accruedFees += fee.toUint128(); + IERC20(UNDERLYING_ASSET).safeTransferFrom(originator, address(this), assetAmount); + + IGhoToken(GHO_TOKEN).mint(address(this), grossAmount); + IGhoToken(GHO_TOKEN).transfer(receiver, ghoBought); + + emit SellAsset(originator, receiver, assetAmount, grossAmount, fee); + return (assetAmount, ghoBought); + } + + /** + * @dev Hook that is called before `sellAsset`. + * @dev This can be used to add custom logic + * @param originator Originator of the request + * @param amount The amount of the underlying asset desired to sell + * @param receiver Recipient address of the GHO being purchased + */ + function _beforeSellAsset( + address originator, + uint256 amount, + address receiver + ) internal virtual {} + + /** + * @dev Returns the amount of GHO sold in exchange of buying underlying asset + * @param assetAmount The amount of underlying asset to buy + * @return The exact amount of asset the user purchases + * @return The total amount of GHO the user sells (gross amount in GHO plus fee) + * @return The gross amount of GHO + * @return The fee amount in GHO, applied on top of gross amount of GHO + */ + function _calculateGhoAmountForBuyAsset( + uint256 assetAmount + ) internal view returns (uint256, uint256, uint256, uint256) { + bool withFee = _feeStrategy != address(0); + // pick the highest GHO amount possible for given asset amount + uint256 grossAmount = IGsmPriceStrategy(PRICE_STRATEGY).getAssetPriceInGho(assetAmount, true); + uint256 fee = withFee ? IGsmFeeStrategy(_feeStrategy).getBuyFee(grossAmount) : 0; + uint256 ghoSold = grossAmount + fee; + uint256 finalGrossAmount = withFee + ? IGsmFeeStrategy(_feeStrategy).getGrossAmountFromTotalBought(ghoSold) + : ghoSold; + // pick the lowest asset amount possible for given GHO amount + uint256 finalAssetAmount = IGsmPriceStrategy(PRICE_STRATEGY).getGhoPriceInAsset( + finalGrossAmount, + false + ); + uint256 finalFee = ghoSold - finalGrossAmount; + return (finalAssetAmount, finalGrossAmount + finalFee, finalGrossAmount, finalFee); + } + + /** + * @dev Returns the amount of GHO bought in exchange of a given amount of underlying asset + * @param assetAmount The amount of underlying asset to sell + * @return The exact amount of asset the user sells + * @return The total amount of GHO the user buys (gross amount in GHO minus fee) + * @return The gross amount of GHO + * @return The fee amount in GHO, applied to the gross amount of GHO + */ + function _calculateGhoAmountForSellAsset( + uint256 assetAmount + ) internal view returns (uint256, uint256, uint256, uint256) { + bool withFee = _feeStrategy != address(0); + // pick the lowest GHO amount possible for given asset amount + uint256 grossAmount = IGsmPriceStrategy(PRICE_STRATEGY).getAssetPriceInGho(assetAmount, false); + uint256 fee = withFee ? IGsmFeeStrategy(_feeStrategy).getSellFee(grossAmount) : 0; + uint256 ghoBought = grossAmount - fee; + uint256 finalGrossAmount = withFee + ? IGsmFeeStrategy(_feeStrategy).getGrossAmountFromTotalSold(ghoBought) + : ghoBought; + // pick the highest asset amount possible for given GHO amount + uint256 finalAssetAmount = IGsmPriceStrategy(PRICE_STRATEGY).getGhoPriceInAsset( + finalGrossAmount, + true + ); + uint256 finalFee = finalGrossAmount - ghoBought; + return (finalAssetAmount, finalGrossAmount - finalFee, finalGrossAmount, finalFee); + } + + /** + * @dev Updates Fee Strategy + * @param feeStrategy The address of the new Fee Strategy + */ + function _updateFeeStrategy(address feeStrategy) internal { + address oldFeeStrategy = _feeStrategy; + _feeStrategy = feeStrategy; + emit FeeStrategyUpdated(oldFeeStrategy, feeStrategy); + } + + /** + * @dev Updates Exposure Cap + * @param exposureCap The value of the new Exposure Cap + */ + function _updateExposureCap(uint128 exposureCap) internal { + uint128 oldExposureCap = _exposureCap; + _exposureCap = exposureCap; + emit ExposureCapUpdated(oldExposureCap, exposureCap); + } + + /** + * @dev Updates GHO Treasury Address + * @param newGhoTreasury The address of the new GHO Treasury + */ + function _updateGhoTreasury(address newGhoTreasury) internal { + require(newGhoTreasury != address(0), 'ZERO_ADDRESS_NOT_VALID'); + address oldGhoTreasury = _ghoTreasury; + _ghoTreasury = newGhoTreasury; + emit GhoTreasuryUpdated(oldGhoTreasury, newGhoTreasury); + } + + /// @inheritdoc VersionedInitializable + function getRevision() internal pure virtual override returns (uint256) { + return GSM_REVISION(); + } +} diff --git a/certora/GSM/mutations/mutants/Gsm/Gsm.sol2 copy.sol b/certora/GSM/mutations/mutants/Gsm/Gsm.sol2 copy.sol new file mode 100644 index 00000000..9b781aed --- /dev/null +++ b/certora/GSM/mutations/mutants/Gsm/Gsm.sol2 copy.sol @@ -0,0 +1,561 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.10; + +import {VersionedInitializable} from '@aave/core-v3/contracts/protocol/libraries/aave-upgradeability/VersionedInitializable.sol'; +import {IERC20} from '@aave/core-v3/contracts/dependencies/openzeppelin/contracts/IERC20.sol'; +import {GPv2SafeERC20} from '@aave/core-v3/contracts/dependencies/gnosis/contracts/GPv2SafeERC20.sol'; +import {EIP712} from '@openzeppelin/contracts/utils/cryptography/EIP712.sol'; +import {SignatureChecker} from '@openzeppelin/contracts/utils/cryptography/SignatureChecker.sol'; +import {SafeCast} from '@openzeppelin/contracts/utils/math/SafeCast.sol'; +import {AccessControl} from '@openzeppelin/contracts/access/AccessControl.sol'; +import {IGhoFacilitator} from '../../gho/interfaces/IGhoFacilitator.sol'; +import {IGhoToken} from '../../gho/interfaces/IGhoToken.sol'; +import {IGsmPriceStrategy} from './priceStrategy/interfaces/IGsmPriceStrategy.sol'; +import {IGsmFeeStrategy} from './feeStrategy/interfaces/IGsmFeeStrategy.sol'; +import {IGsm} from './interfaces/IGsm.sol'; + +/** + * @title Gsm + * @author Aave + * @notice GHO Stability Module. It provides buy/sell facilities to go to/from an underlying asset to/from GHO. + * @dev To be covered by a proxy contract. + */ +contract Gsm is AccessControl, VersionedInitializable, EIP712, IGsm { + using GPv2SafeERC20 for IERC20; + using SafeCast for uint256; + + /// @inheritdoc IGsm + bytes32 public constant CONFIGURATOR_ROLE = keccak256('CONFIGURATOR_ROLE'); + + /// @inheritdoc IGsm + bytes32 public constant TOKEN_RESCUER_ROLE = keccak256('TOKEN_RESCUER_ROLE'); + + /// @inheritdoc IGsm + bytes32 public constant SWAP_FREEZER_ROLE = keccak256('SWAP_FREEZER_ROLE'); + + /// @inheritdoc IGsm + bytes32 public constant LIQUIDATOR_ROLE = keccak256('LIQUIDATOR_ROLE'); + + /// @inheritdoc IGsm + bytes32 public constant BUY_ASSET_WITH_SIG_TYPEHASH = + keccak256( + 'BuyAssetWithSig(address originator,uint256 minAmount,address receiver,uint256 nonce,uint256 deadline)' + ); + + /// @inheritdoc IGsm + bytes32 public constant SELL_ASSET_WITH_SIG_TYPEHASH = + keccak256( + 'SellAssetWithSig(address originator,uint256 maxAmount,address receiver,uint256 nonce,uint256 deadline)' + ); + + /// @inheritdoc IGsm + address public immutable GHO_TOKEN; + + /// @inheritdoc IGsm + address public immutable UNDERLYING_ASSET; + + /// @inheritdoc IGsm + address public immutable PRICE_STRATEGY; + + /// @inheritdoc IGsm + mapping(address => uint256) public nonces; + + address internal _ghoTreasury; + address internal _feeStrategy; + bool internal _isFrozen; + bool internal _isSeized; + uint128 internal _exposureCap; + uint128 internal _currentExposure; + uint128 internal _accruedFees; + + /** + * @dev Require GSM to not be frozen for functions marked by this modifier + */ + modifier notFrozen() { + require(!_isFrozen, 'GSM_FROZEN'); + _; + } + + /** + * @dev Require GSM to not be seized for functions marked by this modifier + */ + modifier notSeized() { + require(!_isSeized, 'GSM_SEIZED'); + _; + } + + /** + * @dev Constructor + * @param ghoToken The address of the GHO token contract + * @param underlyingAsset The address of the collateral asset + * @param priceStrategy The address of the price strategy + */ + constructor(address ghoToken, address underlyingAsset, address priceStrategy) EIP712('GSM', '1') { + require(ghoToken != address(0), 'ZERO_ADDRESS_NOT_VALID'); + require(underlyingAsset != address(0), 'ZERO_ADDRESS_NOT_VALID'); + require( + IGsmPriceStrategy(priceStrategy).UNDERLYING_ASSET() == underlyingAsset, + 'INVALID_PRICE_STRATEGY' + ); + GHO_TOKEN = ghoToken; + UNDERLYING_ASSET = underlyingAsset; + PRICE_STRATEGY = priceStrategy; + } + + /** + * @notice GSM initializer + * @param admin The address of the default admin role + * @param ghoTreasury The address of the GHO treasury + * @param exposureCap Maximum amount of user-supplied underlying asset in GSM + */ + function initialize( + address admin, + address ghoTreasury, + uint128 exposureCap + ) external initializer { + require(admin != address(0), 'ZERO_ADDRESS_NOT_VALID'); + _grantRole(DEFAULT_ADMIN_ROLE, admin); + _grantRole(CONFIGURATOR_ROLE, admin); + _updateGhoTreasury(ghoTreasury); + _updateExposureCap(exposureCap); + } + + /// @inheritdoc IGsm + function buyAsset( + uint256 minAmount, + address receiver + ) external notFrozen notSeized returns (uint256, uint256) { + return _buyAsset(msg.sender, minAmount, receiver); + } + + /// @inheritdoc IGsm + function buyAssetWithSig( + address originator, + uint256 minAmount, + address receiver, + uint256 deadline, + bytes calldata signature + ) external notFrozen notSeized returns (uint256, uint256) { + require(deadline >= block.timestamp, 'SIGNATURE_DEADLINE_EXPIRED'); + bytes32 digest = keccak256( + abi.encode( + '\x19\x01', + _domainSeparatorV4(), + BUY_ASSET_WITH_SIG_TYPEHASH, + abi.encode(originator, minAmount, receiver, nonces[originator]++, deadline) + ) + ); + require( + SignatureChecker.isValidSignatureNow(originator, digest, signature), + 'SIGNATURE_INVALID' + ); + + return _buyAsset(originator, minAmount, receiver); + } + + /// @inheritdoc IGsm + function sellAsset( + uint256 maxAmount, + address receiver + ) external notFrozen notSeized returns (uint256, uint256) { + return _sellAsset(msg.sender, maxAmount, receiver); + } + + /// @inheritdoc IGsm + function sellAssetWithSig( + address originator, + uint256 maxAmount, + address receiver, + uint256 deadline, + bytes calldata signature + ) external notFrozen notSeized returns (uint256, uint256) { + require(deadline >= block.timestamp, 'SIGNATURE_DEADLINE_EXPIRED'); + bytes32 digest = keccak256( + abi.encode( + '\x19\x01', + _domainSeparatorV4(), + SELL_ASSET_WITH_SIG_TYPEHASH, + abi.encode(originator, maxAmount, receiver, nonces[originator]++, deadline) + ) + ); + require( + SignatureChecker.isValidSignatureNow(originator, digest, signature), + 'SIGNATURE_INVALID' + ); + + return _sellAsset(originator, maxAmount, receiver); + } + + /// @inheritdoc IGsm + function rescueTokens( + address token, + address to, + uint256 amount + ) external onlyRole(TOKEN_RESCUER_ROLE) { + require(amount > 0, 'INVALID_AMOUNT'); + if (token == GHO_TOKEN) { + uint256 rescuableBalance = IERC20(token).balanceOf(address(this)) - _accruedFees; + require(rescuableBalance >= amount, 'INSUFFICIENT_GHO_TO_RESCUE'); + } + if (token == UNDERLYING_ASSET) { + uint256 rescuableBalance = IERC20(token).balanceOf(address(this)) - _currentExposure; + require(rescuableBalance >= amount, 'INSUFFICIENT_EXOGENOUS_ASSET_TO_RESCUE'); + } + IERC20(token).safeTransfer(to, amount); + emit TokensRescued(token, to, amount); + } + + /// @inheritdoc IGsm + function setSwapFreeze(bool enable) external onlyRole(SWAP_FREEZER_ROLE) { + if (enable) { + require(!_isFrozen, 'GSM_ALREADY_FROZEN'); + } else { + require(_isFrozen, 'GSM_ALREADY_UNFROZEN'); + } + _isFrozen = enable; + emit SwapFreeze(msg.sender, enable); + } + + /// @inheritdoc IGsm + function seize() external notSeized onlyRole(LIQUIDATOR_ROLE) returns (uint256) { + _isSeized = true; + _currentExposure = 0; + _updateExposureCap(0); + + (, uint256 ghoMinted) = IGhoToken(GHO_TOKEN).getFacilitatorBucket(address(this)); + uint256 underlyingBalance = IERC20(UNDERLYING_ASSET).balanceOf(address(this)); + if (underlyingBalance > 0) { + IERC20(UNDERLYING_ASSET).safeTransfer(_ghoTreasury, underlyingBalance); + } + + emit Seized(msg.sender, _ghoTreasury, underlyingBalance, ghoMinted); + return underlyingBalance; + } + + /// @inheritdoc IGsm + function burnAfterSeize(uint256 amount) external onlyRole(LIQUIDATOR_ROLE) returns (uint256) { + require(_isSeized, 'GSM_NOT_SEIZED'); + require(amount > 0, 'INVALID_AMOUNT'); + + (, uint256 ghoMinted) = IGhoToken(GHO_TOKEN).getFacilitatorBucket(address(this)); + if (amount > ghoMinted) { + amount = ghoMinted; + } + IGhoToken(GHO_TOKEN).transferFrom(msg.sender, address(this), amount); + IGhoToken(GHO_TOKEN).burn(amount); + + emit BurnAfterSeize(msg.sender, amount, (ghoMinted - amount)); + return amount; + } + + /// @inheritdoc IGsm + function updateFeeStrategy(address feeStrategy) external onlyRole(CONFIGURATOR_ROLE) { + _updateFeeStrategy(feeStrategy); + } + + /// @inheritdoc IGsm + function updateExposureCap(uint128 exposureCap) external onlyRole(CONFIGURATOR_ROLE) { + _updateExposureCap(exposureCap); + } + + /// @inheritdoc IGhoFacilitator + function distributeFeesToTreasury() public virtual override { + uint256 accruedFees = _accruedFees; + if (accruedFees > 0) { + _accruedFees = 0; + IERC20(GHO_TOKEN).transfer(_ghoTreasury, accruedFees); + emit FeesDistributedToTreasury(_ghoTreasury, GHO_TOKEN, accruedFees); + } + } + + /// @inheritdoc IGhoFacilitator + function updateGhoTreasury(address newGhoTreasury) external override onlyRole(CONFIGURATOR_ROLE) { + _updateGhoTreasury(newGhoTreasury); + } + + /// @inheritdoc IGsm + function DOMAIN_SEPARATOR() external view returns (bytes32) { + return _domainSeparatorV4(); + } + + /// @inheritdoc IGsm + function getGhoAmountForBuyAsset( + uint256 minAssetAmount + ) external view returns (uint256, uint256, uint256, uint256) { + return _calculateGhoAmountForBuyAsset(minAssetAmount); + } + + /// @inheritdoc IGsm + function getGhoAmountForSellAsset( + uint256 maxAssetAmount + ) external view returns (uint256, uint256, uint256, uint256) { + return _calculateGhoAmountForSellAsset(maxAssetAmount); + } + + /// @inheritdoc IGsm + function getAssetAmountForBuyAsset( + uint256 maxGhoAmount + ) external view returns (uint256, uint256, uint256, uint256) { + bool withFee = _feeStrategy != address(0); + uint256 grossAmount = withFee + ? IGsmFeeStrategy(_feeStrategy).getGrossAmountFromTotalBought(maxGhoAmount) + : maxGhoAmount; + // round down so maxGhoAmount is guaranteed + uint256 assetAmount = IGsmPriceStrategy(PRICE_STRATEGY).getGhoPriceInAsset(grossAmount, false); + uint256 finalGrossAmount = IGsmPriceStrategy(PRICE_STRATEGY).getAssetPriceInGho( + assetAmount, + true // TODO + ); + uint256 finalFee = withFee ? IGsmFeeStrategy(_feeStrategy).getBuyFee(finalGrossAmount) : 0; + return (assetAmount, finalGrossAmount + finalFee, finalGrossAmount, finalFee); + } + + /// @inheritdoc IGsm + function getAssetAmountForSellAsset( + uint256 minGhoAmount + ) external view returns (uint256, uint256, uint256, uint256) { + bool withFee = _feeStrategy != address(0); + uint256 grossAmount = withFee + ? IGsmFeeStrategy(_feeStrategy).getGrossAmountFromTotalSold(minGhoAmount) + : minGhoAmount; + // round up so minGhoAmount is guaranteed + uint256 assetAmount = IGsmPriceStrategy(PRICE_STRATEGY).getGhoPriceInAsset(grossAmount, true); + uint256 finalGrossAmount = IGsmPriceStrategy(PRICE_STRATEGY).getAssetPriceInGho( + assetAmount, + false // TODO + ); + uint256 finalFee = withFee ? IGsmFeeStrategy(_feeStrategy).getSellFee(finalGrossAmount) : 0; + return (assetAmount, finalGrossAmount - finalFee, finalGrossAmount, finalFee); + } + + /// @inheritdoc IGsm + function getAvailableUnderlyingExposure() external view returns (uint256) { + return _exposureCap > _currentExposure ? _exposureCap - _currentExposure : 0; + } + + /// @inheritdoc IGsm + function getAvailableLiquidity() external view returns (uint256) { + return _currentExposure; + } + + /// @inheritdoc IGsm + function getFeeStrategy() external view returns (address) { + return _feeStrategy; + } + + /// @inheritdoc IGsm + function getAccruedFees() external view returns (uint256) { + return _accruedFees; + } + + /// @inheritdoc IGsm + function getIsFrozen() external view returns (bool) { + return _isFrozen; + } + + /// @inheritdoc IGsm + function getIsSeized() external view returns (bool) { + return _isSeized; + } + + /// @inheritdoc IGsm + function canSwap() external view returns (bool) { + return !_isFrozen && !_isSeized; + } + + /// @inheritdoc IGhoFacilitator + function getGhoTreasury() external view override returns (address) { + return _ghoTreasury; + } + + /// @inheritdoc IGsm + function GSM_REVISION() public pure virtual override returns (uint256) { + return 1; + } + + /** + * @dev Buys an underlying asset with GHO + * @param originator The originator of the request + * @param minAmount The minimum amount of the underlying asset desired for purchase + * @param receiver The recipient address of the underlying asset being purchased + * @return The amount of underlying asset bought + * @return The amount of GHO sold by the user + */ + function _buyAsset( + address originator, + uint256 minAmount, + address receiver + ) internal returns (uint256, uint256) { + ( + uint256 assetAmount, + uint256 ghoSold, + uint256 grossAmount, + uint256 fee + ) = _calculateGhoAmountForBuyAsset(minAmount); + + _beforeBuyAsset(originator, assetAmount, receiver); + + require(assetAmount > 0, 'INVALID_AMOUNT'); + require(_currentExposure >= assetAmount, 'INSUFFICIENT_AVAILABLE_EXOGENOUS_ASSET_LIQUIDITY'); + + _currentExposure -= uint128(assetAmount); + /// AssignmentMutation of: _accruedFees += fee.toUint128(); + _accruedFees += 1; + IGhoToken(GHO_TOKEN).transferFrom(originator, address(this), ghoSold); + IGhoToken(GHO_TOKEN).burn(grossAmount); + IERC20(UNDERLYING_ASSET).safeTransfer(receiver, assetAmount); + + emit BuyAsset(originator, receiver, assetAmount, ghoSold, fee); + return (assetAmount, ghoSold); + } + + /** + * @dev Hook that is called before `buyAsset`. + * @dev This can be used to add custom logic + * @param originator Originator of the request + * @param amount The amount of the underlying asset desired for purchase + * @param receiver Recipient address of the underlying asset being purchased + */ + function _beforeBuyAsset(address originator, uint256 amount, address receiver) internal virtual {} + + /** + * @dev Sells an underlying asset for GHO + * @param originator The originator of the request + * @param maxAmount The maximum amount of the underlying asset desired to sell + * @param receiver The recipient address of the GHO being purchased + * @return The amount of underlying asset sold + * @return The amount of GHO bought by the user + */ + function _sellAsset( + address originator, + uint256 maxAmount, + address receiver + ) internal returns (uint256, uint256) { + ( + uint256 assetAmount, + uint256 ghoBought, + uint256 grossAmount, + uint256 fee + ) = _calculateGhoAmountForSellAsset(maxAmount); + + _beforeSellAsset(originator, assetAmount, receiver); + + require(assetAmount > 0, 'INVALID_AMOUNT'); + require(_currentExposure + assetAmount <= _exposureCap, 'EXOGENOUS_ASSET_EXPOSURE_TOO_HIGH'); + + _currentExposure += uint128(assetAmount); + _accruedFees += fee.toUint128(); + IERC20(UNDERLYING_ASSET).safeTransferFrom(originator, address(this), assetAmount); + + IGhoToken(GHO_TOKEN).mint(address(this), grossAmount); + IGhoToken(GHO_TOKEN).transfer(receiver, ghoBought); + + emit SellAsset(originator, receiver, assetAmount, grossAmount, fee); + return (assetAmount, ghoBought); + } + + /** + * @dev Hook that is called before `sellAsset`. + * @dev This can be used to add custom logic + * @param originator Originator of the request + * @param amount The amount of the underlying asset desired to sell + * @param receiver Recipient address of the GHO being purchased + */ + function _beforeSellAsset( + address originator, + uint256 amount, + address receiver + ) internal virtual {} + + /** + * @dev Returns the amount of GHO sold in exchange of buying underlying asset + * @param assetAmount The amount of underlying asset to buy + * @return The exact amount of asset the user purchases + * @return The total amount of GHO the user sells (gross amount in GHO plus fee) + * @return The gross amount of GHO + * @return The fee amount in GHO, applied on top of gross amount of GHO + */ + function _calculateGhoAmountForBuyAsset( + uint256 assetAmount + ) internal view returns (uint256, uint256, uint256, uint256) { + bool withFee = _feeStrategy != address(0); + // pick the highest GHO amount possible for given asset amount + uint256 grossAmount = IGsmPriceStrategy(PRICE_STRATEGY).getAssetPriceInGho(assetAmount, true); + uint256 fee = withFee ? IGsmFeeStrategy(_feeStrategy).getBuyFee(grossAmount) : 0; + uint256 ghoSold = grossAmount + fee; + uint256 finalGrossAmount = withFee + ? IGsmFeeStrategy(_feeStrategy).getGrossAmountFromTotalBought(ghoSold) + : ghoSold; + // pick the lowest asset amount possible for given GHO amount + uint256 finalAssetAmount = IGsmPriceStrategy(PRICE_STRATEGY).getGhoPriceInAsset( + finalGrossAmount, + false + ); + uint256 finalFee = ghoSold - finalGrossAmount; + return (finalAssetAmount, finalGrossAmount + finalFee, finalGrossAmount, finalFee); + } + + /** + * @dev Returns the amount of GHO bought in exchange of a given amount of underlying asset + * @param assetAmount The amount of underlying asset to sell + * @return The exact amount of asset the user sells + * @return The total amount of GHO the user buys (gross amount in GHO minus fee) + * @return The gross amount of GHO + * @return The fee amount in GHO, applied to the gross amount of GHO + */ + function _calculateGhoAmountForSellAsset( + uint256 assetAmount + ) internal view returns (uint256, uint256, uint256, uint256) { + bool withFee = _feeStrategy != address(0); + // pick the lowest GHO amount possible for given asset amount + uint256 grossAmount = IGsmPriceStrategy(PRICE_STRATEGY).getAssetPriceInGho(assetAmount, false); + uint256 fee = withFee ? IGsmFeeStrategy(_feeStrategy).getSellFee(grossAmount) : 0; + uint256 ghoBought = grossAmount - fee; + uint256 finalGrossAmount = withFee + ? IGsmFeeStrategy(_feeStrategy).getGrossAmountFromTotalSold(ghoBought) + : ghoBought; + // pick the highest asset amount possible for given GHO amount + uint256 finalAssetAmount = IGsmPriceStrategy(PRICE_STRATEGY).getGhoPriceInAsset( + finalGrossAmount, + true + ); + uint256 finalFee = finalGrossAmount - ghoBought; + return (finalAssetAmount, finalGrossAmount - finalFee, finalGrossAmount, finalFee); + } + + /** + * @dev Updates Fee Strategy + * @param feeStrategy The address of the new Fee Strategy + */ + function _updateFeeStrategy(address feeStrategy) internal { + address oldFeeStrategy = _feeStrategy; + _feeStrategy = feeStrategy; + emit FeeStrategyUpdated(oldFeeStrategy, feeStrategy); + } + + /** + * @dev Updates Exposure Cap + * @param exposureCap The value of the new Exposure Cap + */ + function _updateExposureCap(uint128 exposureCap) internal { + uint128 oldExposureCap = _exposureCap; + _exposureCap = exposureCap; + emit ExposureCapUpdated(oldExposureCap, exposureCap); + } + + /** + * @dev Updates GHO Treasury Address + * @param newGhoTreasury The address of the new GHO Treasury + */ + function _updateGhoTreasury(address newGhoTreasury) internal { + require(newGhoTreasury != address(0), 'ZERO_ADDRESS_NOT_VALID'); + address oldGhoTreasury = _ghoTreasury; + _ghoTreasury = newGhoTreasury; + emit GhoTreasuryUpdated(oldGhoTreasury, newGhoTreasury); + } + + /// @inheritdoc VersionedInitializable + function getRevision() internal pure virtual override returns (uint256) { + return GSM_REVISION(); + } +} diff --git a/certora/GSM/mutations/mutants/Gsm/Gsm.sol2.sol b/certora/GSM/mutations/mutants/Gsm/Gsm.sol2.sol new file mode 100644 index 00000000..37499cd6 --- /dev/null +++ b/certora/GSM/mutations/mutants/Gsm/Gsm.sol2.sol @@ -0,0 +1,561 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.10; + +import {VersionedInitializable} from '@aave/core-v3/contracts/protocol/libraries/aave-upgradeability/VersionedInitializable.sol'; +import {IERC20} from '@aave/core-v3/contracts/dependencies/openzeppelin/contracts/IERC20.sol'; +import {GPv2SafeERC20} from '@aave/core-v3/contracts/dependencies/gnosis/contracts/GPv2SafeERC20.sol'; +import {EIP712} from '@openzeppelin/contracts/utils/cryptography/EIP712.sol'; +import {SignatureChecker} from '@openzeppelin/contracts/utils/cryptography/SignatureChecker.sol'; +import {SafeCast} from '@openzeppelin/contracts/utils/math/SafeCast.sol'; +import {AccessControl} from '@openzeppelin/contracts/access/AccessControl.sol'; +import {IGhoFacilitator} from '../../gho/interfaces/IGhoFacilitator.sol'; +import {IGhoToken} from '../../gho/interfaces/IGhoToken.sol'; +import {IGsmPriceStrategy} from './priceStrategy/interfaces/IGsmPriceStrategy.sol'; +import {IGsmFeeStrategy} from './feeStrategy/interfaces/IGsmFeeStrategy.sol'; +import {IGsm} from './interfaces/IGsm.sol'; + +/** + * @title Gsm + * @author Aave + * @notice GHO Stability Module. It provides buy/sell facilities to go to/from an underlying asset to/from GHO. + * @dev To be covered by a proxy contract. + */ +contract Gsm is AccessControl, VersionedInitializable, EIP712, IGsm { + using GPv2SafeERC20 for IERC20; + using SafeCast for uint256; + + /// @inheritdoc IGsm + bytes32 public constant CONFIGURATOR_ROLE = keccak256('CONFIGURATOR_ROLE'); + + /// @inheritdoc IGsm + bytes32 public constant TOKEN_RESCUER_ROLE = keccak256('TOKEN_RESCUER_ROLE'); + + /// @inheritdoc IGsm + bytes32 public constant SWAP_FREEZER_ROLE = keccak256('SWAP_FREEZER_ROLE'); + + /// @inheritdoc IGsm + bytes32 public constant LIQUIDATOR_ROLE = keccak256('LIQUIDATOR_ROLE'); + + /// @inheritdoc IGsm + bytes32 public constant BUY_ASSET_WITH_SIG_TYPEHASH = + keccak256( + 'BuyAssetWithSig(address originator,uint256 minAmount,address receiver,uint256 nonce,uint256 deadline)' + ); + + /// @inheritdoc IGsm + bytes32 public constant SELL_ASSET_WITH_SIG_TYPEHASH = + keccak256( + 'SellAssetWithSig(address originator,uint256 maxAmount,address receiver,uint256 nonce,uint256 deadline)' + ); + + /// @inheritdoc IGsm + address public immutable GHO_TOKEN; + + /// @inheritdoc IGsm + address public immutable UNDERLYING_ASSET; + + /// @inheritdoc IGsm + address public immutable PRICE_STRATEGY; + + /// @inheritdoc IGsm + mapping(address => uint256) public nonces; + + address internal _ghoTreasury; + address internal _feeStrategy; + bool internal _isFrozen; + bool internal _isSeized; + uint128 internal _exposureCap; + uint128 internal _currentExposure; + uint128 internal _accruedFees; + + /** + * @dev Require GSM to not be frozen for functions marked by this modifier + */ + modifier notFrozen() { + require(!_isFrozen, 'GSM_FROZEN'); + _; + } + + /** + * @dev Require GSM to not be seized for functions marked by this modifier + */ + modifier notSeized() { + require(!_isSeized, 'GSM_SEIZED'); + _; + } + + /** + * @dev Constructor + * @param ghoToken The address of the GHO token contract + * @param underlyingAsset The address of the collateral asset + * @param priceStrategy The address of the price strategy + */ + constructor(address ghoToken, address underlyingAsset, address priceStrategy) EIP712('GSM', '1') { + require(ghoToken != address(0), 'ZERO_ADDRESS_NOT_VALID'); + require(underlyingAsset != address(0), 'ZERO_ADDRESS_NOT_VALID'); + require( + IGsmPriceStrategy(priceStrategy).UNDERLYING_ASSET() == underlyingAsset, + 'INVALID_PRICE_STRATEGY' + ); + GHO_TOKEN = ghoToken; + UNDERLYING_ASSET = underlyingAsset; + PRICE_STRATEGY = priceStrategy; + } + + /** + * @notice GSM initializer + * @param admin The address of the default admin role + * @param ghoTreasury The address of the GHO treasury + * @param exposureCap Maximum amount of user-supplied underlying asset in GSM + */ + function initialize( + address admin, + address ghoTreasury, + uint128 exposureCap + ) external initializer { + require(admin != address(0), 'ZERO_ADDRESS_NOT_VALID'); + _grantRole(DEFAULT_ADMIN_ROLE, admin); + _grantRole(CONFIGURATOR_ROLE, admin); + _updateGhoTreasury(ghoTreasury); + _updateExposureCap(exposureCap); + } + + /// @inheritdoc IGsm + function buyAsset( + uint256 minAmount, + address receiver + ) external notFrozen notSeized returns (uint256, uint256) { + return _buyAsset(msg.sender, minAmount, receiver); + } + + /// @inheritdoc IGsm + function buyAssetWithSig( + address originator, + uint256 minAmount, + address receiver, + uint256 deadline, + bytes calldata signature + ) external notFrozen notSeized returns (uint256, uint256) { + require(deadline >= block.timestamp, 'SIGNATURE_DEADLINE_EXPIRED'); + bytes32 digest = keccak256( + abi.encode( + '\x19\x01', + _domainSeparatorV4(), + BUY_ASSET_WITH_SIG_TYPEHASH, + abi.encode(originator, minAmount, receiver, nonces[originator]++, deadline) + ) + ); + require( + SignatureChecker.isValidSignatureNow(originator, digest, signature), + 'SIGNATURE_INVALID' + ); + + return _buyAsset(originator, minAmount, receiver); + } + + /// @inheritdoc IGsm + function sellAsset( + uint256 maxAmount, + address receiver + ) external notFrozen notSeized returns (uint256, uint256) { + return _sellAsset(msg.sender, maxAmount, receiver); + } + + /// @inheritdoc IGsm + function sellAssetWithSig( + address originator, + uint256 maxAmount, + address receiver, + uint256 deadline, + bytes calldata signature + ) external notFrozen notSeized returns (uint256, uint256) { + require(deadline >= block.timestamp, 'SIGNATURE_DEADLINE_EXPIRED'); + bytes32 digest = keccak256( + abi.encode( + '\x19\x01', + _domainSeparatorV4(), + SELL_ASSET_WITH_SIG_TYPEHASH, + abi.encode(originator, maxAmount, receiver, nonces[originator]++, deadline) + ) + ); + require( + SignatureChecker.isValidSignatureNow(originator, digest, signature), + 'SIGNATURE_INVALID' + ); + + return _sellAsset(originator, maxAmount, receiver); + } + + /// @inheritdoc IGsm + function rescueTokens( + address token, + address to, + uint256 amount + ) external onlyRole(TOKEN_RESCUER_ROLE) { + require(amount > 0, 'INVALID_AMOUNT'); + if (token == GHO_TOKEN) { + uint256 rescuableBalance = IERC20(token).balanceOf(address(this)) - _accruedFees; + require(rescuableBalance >= amount, 'INSUFFICIENT_GHO_TO_RESCUE'); + } + if (token == UNDERLYING_ASSET) { + uint256 rescuableBalance = IERC20(token).balanceOf(address(this)) - _currentExposure; + require(rescuableBalance >= amount, 'INSUFFICIENT_EXOGENOUS_ASSET_TO_RESCUE'); + } + IERC20(token).safeTransfer(to, amount); + emit TokensRescued(token, to, amount); + } + + /// @inheritdoc IGsm + function setSwapFreeze(bool enable) external onlyRole(SWAP_FREEZER_ROLE) { + if (enable) { + require(!_isFrozen, 'GSM_ALREADY_FROZEN'); + } else { + require(_isFrozen, 'GSM_ALREADY_UNFROZEN'); + } + _isFrozen = enable; + emit SwapFreeze(msg.sender, enable); + } + + /// @inheritdoc IGsm + function seize() external notSeized onlyRole(LIQUIDATOR_ROLE) returns (uint256) { + _isSeized = true; + _currentExposure = 0; + _updateExposureCap(0); + + (, uint256 ghoMinted) = IGhoToken(GHO_TOKEN).getFacilitatorBucket(address(this)); + uint256 underlyingBalance = IERC20(UNDERLYING_ASSET).balanceOf(address(this)); + if (underlyingBalance > 0) { + IERC20(UNDERLYING_ASSET).safeTransfer(_ghoTreasury, underlyingBalance); + } + + emit Seized(msg.sender, _ghoTreasury, underlyingBalance, ghoMinted); + return underlyingBalance; + } + + /// @inheritdoc IGsm + function burnAfterSeize(uint256 amount) external onlyRole(LIQUIDATOR_ROLE) returns (uint256) { + require(_isSeized, 'GSM_NOT_SEIZED'); + require(amount > 0, 'INVALID_AMOUNT'); + + (, uint256 ghoMinted) = IGhoToken(GHO_TOKEN).getFacilitatorBucket(address(this)); + if (amount > ghoMinted) { + amount = ghoMinted; + } + IGhoToken(GHO_TOKEN).transferFrom(msg.sender, address(this), amount); + IGhoToken(GHO_TOKEN).burn(amount); + + emit BurnAfterSeize(msg.sender, amount, (ghoMinted - amount)); + return amount; + } + + /// @inheritdoc IGsm + function updateFeeStrategy(address feeStrategy) external onlyRole(CONFIGURATOR_ROLE) { + _updateFeeStrategy(feeStrategy); + } + + /// @inheritdoc IGsm + function updateExposureCap(uint128 exposureCap) external onlyRole(CONFIGURATOR_ROLE) { + _updateExposureCap(exposureCap); + } + + /// @inheritdoc IGhoFacilitator + function distributeFeesToTreasury() public virtual override { + uint256 accruedFees = _accruedFees; + if (accruedFees > 0) { + _accruedFees = 0; + IERC20(GHO_TOKEN).transfer(_ghoTreasury, accruedFees); + emit FeesDistributedToTreasury(_ghoTreasury, GHO_TOKEN, accruedFees); + } + } + + /// @inheritdoc IGhoFacilitator + function updateGhoTreasury(address newGhoTreasury) external override onlyRole(CONFIGURATOR_ROLE) { + _updateGhoTreasury(newGhoTreasury); + } + + /// @inheritdoc IGsm + function DOMAIN_SEPARATOR() external view returns (bytes32) { + return _domainSeparatorV4(); + } + + /// @inheritdoc IGsm + function getGhoAmountForBuyAsset( + uint256 minAssetAmount + ) external view returns (uint256, uint256, uint256, uint256) { + return _calculateGhoAmountForBuyAsset(minAssetAmount); + } + + /// @inheritdoc IGsm + function getGhoAmountForSellAsset( + uint256 maxAssetAmount + ) external view returns (uint256, uint256, uint256, uint256) { + return _calculateGhoAmountForSellAsset(maxAssetAmount); + } + + /// @inheritdoc IGsm + function getAssetAmountForBuyAsset( + uint256 maxGhoAmount + ) external view returns (uint256, uint256, uint256, uint256) { + bool withFee = _feeStrategy != address(0); + uint256 grossAmount = withFee + ? IGsmFeeStrategy(_feeStrategy).getGrossAmountFromTotalBought(maxGhoAmount) + : maxGhoAmount; + // round down so maxGhoAmount is guaranteed + uint256 assetAmount = IGsmPriceStrategy(PRICE_STRATEGY).getGhoPriceInAsset(grossAmount, false); + uint256 finalGrossAmount = IGsmPriceStrategy(PRICE_STRATEGY).getAssetPriceInGho( + assetAmount, + true // TODO + ); + uint256 finalFee = withFee ? IGsmFeeStrategy(_feeStrategy).getBuyFee(finalGrossAmount) : 0; + return (assetAmount, finalGrossAmount + finalFee, finalGrossAmount, finalFee); + } + + /// @inheritdoc IGsm + function getAssetAmountForSellAsset( + uint256 minGhoAmount + ) external view returns (uint256, uint256, uint256, uint256) { + bool withFee = _feeStrategy != address(0); + uint256 grossAmount = withFee + ? IGsmFeeStrategy(_feeStrategy).getGrossAmountFromTotalSold(minGhoAmount) + : minGhoAmount; + // round up so minGhoAmount is guaranteed + uint256 assetAmount = IGsmPriceStrategy(PRICE_STRATEGY).getGhoPriceInAsset(grossAmount, true); + uint256 finalGrossAmount = IGsmPriceStrategy(PRICE_STRATEGY).getAssetPriceInGho( + assetAmount, + false // TODO + ); + uint256 finalFee = withFee ? IGsmFeeStrategy(_feeStrategy).getSellFee(finalGrossAmount) : 0; + return (assetAmount, finalGrossAmount - finalFee, finalGrossAmount, finalFee); + } + + /// @inheritdoc IGsm + function getAvailableUnderlyingExposure() external view returns (uint256) { + return _exposureCap > _currentExposure ? _exposureCap - _currentExposure : 0; + } + + /// @inheritdoc IGsm + function getAvailableLiquidity() external view returns (uint256) { + return _currentExposure; + } + + /// @inheritdoc IGsm + function getFeeStrategy() external view returns (address) { + return _feeStrategy; + } + + /// @inheritdoc IGsm + function getAccruedFees() external view returns (uint256) { + return _accruedFees; + } + + /// @inheritdoc IGsm + function getIsFrozen() external view returns (bool) { + return _isFrozen; + } + + /// @inheritdoc IGsm + function getIsSeized() external view returns (bool) { + return _isSeized; + } + + /// @inheritdoc IGsm + function canSwap() external view returns (bool) { + return !_isFrozen && !_isSeized; + } + + /// @inheritdoc IGhoFacilitator + function getGhoTreasury() external view override returns (address) { + return _ghoTreasury; + } + + /// @inheritdoc IGsm + function GSM_REVISION() public pure virtual override returns (uint256) { + return 1; + } + + /** + * @dev Buys an underlying asset with GHO + * @param originator The originator of the request + * @param minAmount The minimum amount of the underlying asset desired for purchase + * @param receiver The recipient address of the underlying asset being purchased + * @return The amount of underlying asset bought + * @return The amount of GHO sold by the user + */ + function _buyAsset( + address originator, + uint256 minAmount, + address receiver + ) internal returns (uint256, uint256) { + ( + uint256 assetAmount, + uint256 ghoSold, + uint256 grossAmount, + uint256 fee + ) = _calculateGhoAmountForBuyAsset(minAmount); + + _beforeBuyAsset(originator, assetAmount, receiver); + + require(assetAmount > 0, 'INVALID_AMOUNT'); + require(_currentExposure >= assetAmount, 'INSUFFICIENT_AVAILABLE_EXOGENOUS_ASSET_LIQUIDITY'); + + _currentExposure -= uint128(assetAmount); + _accruedFees += fee.toUint128(); + IGhoToken(GHO_TOKEN).transferFrom(originator, address(this), ghoSold); + IGhoToken(GHO_TOKEN).burn(grossAmount); + IERC20(UNDERLYING_ASSET).safeTransfer(receiver, assetAmount); + + emit BuyAsset(originator, receiver, assetAmount, ghoSold, fee); + return (assetAmount, ghoSold); + } + + /** + * @dev Hook that is called before `buyAsset`. + * @dev This can be used to add custom logic + * @param originator Originator of the request + * @param amount The amount of the underlying asset desired for purchase + * @param receiver Recipient address of the underlying asset being purchased + */ + function _beforeBuyAsset(address originator, uint256 amount, address receiver) internal virtual {} + + /** + * @dev Sells an underlying asset for GHO + * @param originator The originator of the request + * @param maxAmount The maximum amount of the underlying asset desired to sell + * @param receiver The recipient address of the GHO being purchased + * @return The amount of underlying asset sold + * @return The amount of GHO bought by the user + */ + function _sellAsset( + address originator, + uint256 maxAmount, + address receiver + ) internal returns (uint256, uint256) { + ( + uint256 assetAmount, + uint256 ghoBought, + uint256 grossAmount, + uint256 fee + ) = _calculateGhoAmountForSellAsset(maxAmount); + + _beforeSellAsset(originator, assetAmount, receiver); + + require(assetAmount > 0, 'INVALID_AMOUNT'); + require(_currentExposure + assetAmount <= _exposureCap, 'EXOGENOUS_ASSET_EXPOSURE_TOO_HIGH'); + + /// AssignmentMutation of: _currentExposure += uint128(assetAmount); + _currentExposure += 1; + _accruedFees += fee.toUint128(); + IERC20(UNDERLYING_ASSET).safeTransferFrom(originator, address(this), assetAmount); + + IGhoToken(GHO_TOKEN).mint(address(this), grossAmount); + IGhoToken(GHO_TOKEN).transfer(receiver, ghoBought); + + emit SellAsset(originator, receiver, assetAmount, grossAmount, fee); + return (assetAmount, ghoBought); + } + + /** + * @dev Hook that is called before `sellAsset`. + * @dev This can be used to add custom logic + * @param originator Originator of the request + * @param amount The amount of the underlying asset desired to sell + * @param receiver Recipient address of the GHO being purchased + */ + function _beforeSellAsset( + address originator, + uint256 amount, + address receiver + ) internal virtual {} + + /** + * @dev Returns the amount of GHO sold in exchange of buying underlying asset + * @param assetAmount The amount of underlying asset to buy + * @return The exact amount of asset the user purchases + * @return The total amount of GHO the user sells (gross amount in GHO plus fee) + * @return The gross amount of GHO + * @return The fee amount in GHO, applied on top of gross amount of GHO + */ + function _calculateGhoAmountForBuyAsset( + uint256 assetAmount + ) internal view returns (uint256, uint256, uint256, uint256) { + bool withFee = _feeStrategy != address(0); + // pick the highest GHO amount possible for given asset amount + uint256 grossAmount = IGsmPriceStrategy(PRICE_STRATEGY).getAssetPriceInGho(assetAmount, true); + uint256 fee = withFee ? IGsmFeeStrategy(_feeStrategy).getBuyFee(grossAmount) : 0; + uint256 ghoSold = grossAmount + fee; + uint256 finalGrossAmount = withFee + ? IGsmFeeStrategy(_feeStrategy).getGrossAmountFromTotalBought(ghoSold) + : ghoSold; + // pick the lowest asset amount possible for given GHO amount + uint256 finalAssetAmount = IGsmPriceStrategy(PRICE_STRATEGY).getGhoPriceInAsset( + finalGrossAmount, + false + ); + uint256 finalFee = ghoSold - finalGrossAmount; + return (finalAssetAmount, finalGrossAmount + finalFee, finalGrossAmount, finalFee); + } + + /** + * @dev Returns the amount of GHO bought in exchange of a given amount of underlying asset + * @param assetAmount The amount of underlying asset to sell + * @return The exact amount of asset the user sells + * @return The total amount of GHO the user buys (gross amount in GHO minus fee) + * @return The gross amount of GHO + * @return The fee amount in GHO, applied to the gross amount of GHO + */ + function _calculateGhoAmountForSellAsset( + uint256 assetAmount + ) internal view returns (uint256, uint256, uint256, uint256) { + bool withFee = _feeStrategy != address(0); + // pick the lowest GHO amount possible for given asset amount + uint256 grossAmount = IGsmPriceStrategy(PRICE_STRATEGY).getAssetPriceInGho(assetAmount, false); + uint256 fee = withFee ? IGsmFeeStrategy(_feeStrategy).getSellFee(grossAmount) : 0; + uint256 ghoBought = grossAmount - fee; + uint256 finalGrossAmount = withFee + ? IGsmFeeStrategy(_feeStrategy).getGrossAmountFromTotalSold(ghoBought) + : ghoBought; + // pick the highest asset amount possible for given GHO amount + uint256 finalAssetAmount = IGsmPriceStrategy(PRICE_STRATEGY).getGhoPriceInAsset( + finalGrossAmount, + true + ); + uint256 finalFee = finalGrossAmount - ghoBought; + return (finalAssetAmount, finalGrossAmount - finalFee, finalGrossAmount, finalFee); + } + + /** + * @dev Updates Fee Strategy + * @param feeStrategy The address of the new Fee Strategy + */ + function _updateFeeStrategy(address feeStrategy) internal { + address oldFeeStrategy = _feeStrategy; + _feeStrategy = feeStrategy; + emit FeeStrategyUpdated(oldFeeStrategy, feeStrategy); + } + + /** + * @dev Updates Exposure Cap + * @param exposureCap The value of the new Exposure Cap + */ + function _updateExposureCap(uint128 exposureCap) internal { + uint128 oldExposureCap = _exposureCap; + _exposureCap = exposureCap; + emit ExposureCapUpdated(oldExposureCap, exposureCap); + } + + /** + * @dev Updates GHO Treasury Address + * @param newGhoTreasury The address of the new GHO Treasury + */ + function _updateGhoTreasury(address newGhoTreasury) internal { + require(newGhoTreasury != address(0), 'ZERO_ADDRESS_NOT_VALID'); + address oldGhoTreasury = _ghoTreasury; + _ghoTreasury = newGhoTreasury; + emit GhoTreasuryUpdated(oldGhoTreasury, newGhoTreasury); + } + + /// @inheritdoc VersionedInitializable + function getRevision() internal pure virtual override returns (uint256) { + return GSM_REVISION(); + } +} diff --git a/certora/GSM/mutations/mutants/Gsm/Gsm.sol3 copy.sol b/certora/GSM/mutations/mutants/Gsm/Gsm.sol3 copy.sol new file mode 100644 index 00000000..6364170b --- /dev/null +++ b/certora/GSM/mutations/mutants/Gsm/Gsm.sol3 copy.sol @@ -0,0 +1,561 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.10; + +import {VersionedInitializable} from '@aave/core-v3/contracts/protocol/libraries/aave-upgradeability/VersionedInitializable.sol'; +import {IERC20} from '@aave/core-v3/contracts/dependencies/openzeppelin/contracts/IERC20.sol'; +import {GPv2SafeERC20} from '@aave/core-v3/contracts/dependencies/gnosis/contracts/GPv2SafeERC20.sol'; +import {EIP712} from '@openzeppelin/contracts/utils/cryptography/EIP712.sol'; +import {SignatureChecker} from '@openzeppelin/contracts/utils/cryptography/SignatureChecker.sol'; +import {SafeCast} from '@openzeppelin/contracts/utils/math/SafeCast.sol'; +import {AccessControl} from '@openzeppelin/contracts/access/AccessControl.sol'; +import {IGhoFacilitator} from '../../gho/interfaces/IGhoFacilitator.sol'; +import {IGhoToken} from '../../gho/interfaces/IGhoToken.sol'; +import {IGsmPriceStrategy} from './priceStrategy/interfaces/IGsmPriceStrategy.sol'; +import {IGsmFeeStrategy} from './feeStrategy/interfaces/IGsmFeeStrategy.sol'; +import {IGsm} from './interfaces/IGsm.sol'; + +/** + * @title Gsm + * @author Aave + * @notice GHO Stability Module. It provides buy/sell facilities to go to/from an underlying asset to/from GHO. + * @dev To be covered by a proxy contract. + */ +contract Gsm is AccessControl, VersionedInitializable, EIP712, IGsm { + using GPv2SafeERC20 for IERC20; + using SafeCast for uint256; + + /// @inheritdoc IGsm + bytes32 public constant CONFIGURATOR_ROLE = keccak256('CONFIGURATOR_ROLE'); + + /// @inheritdoc IGsm + bytes32 public constant TOKEN_RESCUER_ROLE = keccak256('TOKEN_RESCUER_ROLE'); + + /// @inheritdoc IGsm + bytes32 public constant SWAP_FREEZER_ROLE = keccak256('SWAP_FREEZER_ROLE'); + + /// @inheritdoc IGsm + bytes32 public constant LIQUIDATOR_ROLE = keccak256('LIQUIDATOR_ROLE'); + + /// @inheritdoc IGsm + bytes32 public constant BUY_ASSET_WITH_SIG_TYPEHASH = + keccak256( + 'BuyAssetWithSig(address originator,uint256 minAmount,address receiver,uint256 nonce,uint256 deadline)' + ); + + /// @inheritdoc IGsm + bytes32 public constant SELL_ASSET_WITH_SIG_TYPEHASH = + keccak256( + 'SellAssetWithSig(address originator,uint256 maxAmount,address receiver,uint256 nonce,uint256 deadline)' + ); + + /// @inheritdoc IGsm + address public immutable GHO_TOKEN; + + /// @inheritdoc IGsm + address public immutable UNDERLYING_ASSET; + + /// @inheritdoc IGsm + address public immutable PRICE_STRATEGY; + + /// @inheritdoc IGsm + mapping(address => uint256) public nonces; + + address internal _ghoTreasury; + address internal _feeStrategy; + bool internal _isFrozen; + bool internal _isSeized; + uint128 internal _exposureCap; + uint128 internal _currentExposure; + uint128 internal _accruedFees; + + /** + * @dev Require GSM to not be frozen for functions marked by this modifier + */ + modifier notFrozen() { + require(!_isFrozen, 'GSM_FROZEN'); + _; + } + + /** + * @dev Require GSM to not be seized for functions marked by this modifier + */ + modifier notSeized() { + /// SwapLinesMutation of: require(!_isSeized, 'GSM_SEIZED'); + _; + require(!_isSeized, 'GSM_SEIZED'); + } + + /** + * @dev Constructor + * @param ghoToken The address of the GHO token contract + * @param underlyingAsset The address of the collateral asset + * @param priceStrategy The address of the price strategy + */ + constructor(address ghoToken, address underlyingAsset, address priceStrategy) EIP712('GSM', '1') { + require(ghoToken != address(0), 'ZERO_ADDRESS_NOT_VALID'); + require(underlyingAsset != address(0), 'ZERO_ADDRESS_NOT_VALID'); + require( + IGsmPriceStrategy(priceStrategy).UNDERLYING_ASSET() == underlyingAsset, + 'INVALID_PRICE_STRATEGY' + ); + GHO_TOKEN = ghoToken; + UNDERLYING_ASSET = underlyingAsset; + PRICE_STRATEGY = priceStrategy; + } + + /** + * @notice GSM initializer + * @param admin The address of the default admin role + * @param ghoTreasury The address of the GHO treasury + * @param exposureCap Maximum amount of user-supplied underlying asset in GSM + */ + function initialize( + address admin, + address ghoTreasury, + uint128 exposureCap + ) external initializer { + require(admin != address(0), 'ZERO_ADDRESS_NOT_VALID'); + _grantRole(DEFAULT_ADMIN_ROLE, admin); + _grantRole(CONFIGURATOR_ROLE, admin); + _updateGhoTreasury(ghoTreasury); + _updateExposureCap(exposureCap); + } + + /// @inheritdoc IGsm + function buyAsset( + uint256 minAmount, + address receiver + ) external notFrozen notSeized returns (uint256, uint256) { + return _buyAsset(msg.sender, minAmount, receiver); + } + + /// @inheritdoc IGsm + function buyAssetWithSig( + address originator, + uint256 minAmount, + address receiver, + uint256 deadline, + bytes calldata signature + ) external notFrozen notSeized returns (uint256, uint256) { + require(deadline >= block.timestamp, 'SIGNATURE_DEADLINE_EXPIRED'); + bytes32 digest = keccak256( + abi.encode( + '\x19\x01', + _domainSeparatorV4(), + BUY_ASSET_WITH_SIG_TYPEHASH, + abi.encode(originator, minAmount, receiver, nonces[originator]++, deadline) + ) + ); + require( + SignatureChecker.isValidSignatureNow(originator, digest, signature), + 'SIGNATURE_INVALID' + ); + + return _buyAsset(originator, minAmount, receiver); + } + + /// @inheritdoc IGsm + function sellAsset( + uint256 maxAmount, + address receiver + ) external notFrozen notSeized returns (uint256, uint256) { + return _sellAsset(msg.sender, maxAmount, receiver); + } + + /// @inheritdoc IGsm + function sellAssetWithSig( + address originator, + uint256 maxAmount, + address receiver, + uint256 deadline, + bytes calldata signature + ) external notFrozen notSeized returns (uint256, uint256) { + require(deadline >= block.timestamp, 'SIGNATURE_DEADLINE_EXPIRED'); + bytes32 digest = keccak256( + abi.encode( + '\x19\x01', + _domainSeparatorV4(), + SELL_ASSET_WITH_SIG_TYPEHASH, + abi.encode(originator, maxAmount, receiver, nonces[originator]++, deadline) + ) + ); + require( + SignatureChecker.isValidSignatureNow(originator, digest, signature), + 'SIGNATURE_INVALID' + ); + + return _sellAsset(originator, maxAmount, receiver); + } + + /// @inheritdoc IGsm + function rescueTokens( + address token, + address to, + uint256 amount + ) external onlyRole(TOKEN_RESCUER_ROLE) { + require(amount > 0, 'INVALID_AMOUNT'); + if (token == GHO_TOKEN) { + uint256 rescuableBalance = IERC20(token).balanceOf(address(this)) - _accruedFees; + require(rescuableBalance >= amount, 'INSUFFICIENT_GHO_TO_RESCUE'); + } + if (token == UNDERLYING_ASSET) { + uint256 rescuableBalance = IERC20(token).balanceOf(address(this)) - _currentExposure; + require(rescuableBalance >= amount, 'INSUFFICIENT_EXOGENOUS_ASSET_TO_RESCUE'); + } + IERC20(token).safeTransfer(to, amount); + emit TokensRescued(token, to, amount); + } + + /// @inheritdoc IGsm + function setSwapFreeze(bool enable) external onlyRole(SWAP_FREEZER_ROLE) { + if (enable) { + require(!_isFrozen, 'GSM_ALREADY_FROZEN'); + } else { + require(_isFrozen, 'GSM_ALREADY_UNFROZEN'); + } + _isFrozen = enable; + emit SwapFreeze(msg.sender, enable); + } + + /// @inheritdoc IGsm + function seize() external notSeized onlyRole(LIQUIDATOR_ROLE) returns (uint256) { + _isSeized = true; + _currentExposure = 0; + _updateExposureCap(0); + + (, uint256 ghoMinted) = IGhoToken(GHO_TOKEN).getFacilitatorBucket(address(this)); + uint256 underlyingBalance = IERC20(UNDERLYING_ASSET).balanceOf(address(this)); + if (underlyingBalance > 0) { + IERC20(UNDERLYING_ASSET).safeTransfer(_ghoTreasury, underlyingBalance); + } + + emit Seized(msg.sender, _ghoTreasury, underlyingBalance, ghoMinted); + return underlyingBalance; + } + + /// @inheritdoc IGsm + function burnAfterSeize(uint256 amount) external onlyRole(LIQUIDATOR_ROLE) returns (uint256) { + require(_isSeized, 'GSM_NOT_SEIZED'); + require(amount > 0, 'INVALID_AMOUNT'); + + (, uint256 ghoMinted) = IGhoToken(GHO_TOKEN).getFacilitatorBucket(address(this)); + if (amount > ghoMinted) { + amount = ghoMinted; + } + IGhoToken(GHO_TOKEN).transferFrom(msg.sender, address(this), amount); + IGhoToken(GHO_TOKEN).burn(amount); + + emit BurnAfterSeize(msg.sender, amount, (ghoMinted - amount)); + return amount; + } + + /// @inheritdoc IGsm + function updateFeeStrategy(address feeStrategy) external onlyRole(CONFIGURATOR_ROLE) { + _updateFeeStrategy(feeStrategy); + } + + /// @inheritdoc IGsm + function updateExposureCap(uint128 exposureCap) external onlyRole(CONFIGURATOR_ROLE) { + _updateExposureCap(exposureCap); + } + + /// @inheritdoc IGhoFacilitator + function distributeFeesToTreasury() public virtual override { + uint256 accruedFees = _accruedFees; + if (accruedFees > 0) { + _accruedFees = 0; + IERC20(GHO_TOKEN).transfer(_ghoTreasury, accruedFees); + emit FeesDistributedToTreasury(_ghoTreasury, GHO_TOKEN, accruedFees); + } + } + + /// @inheritdoc IGhoFacilitator + function updateGhoTreasury(address newGhoTreasury) external override onlyRole(CONFIGURATOR_ROLE) { + _updateGhoTreasury(newGhoTreasury); + } + + /// @inheritdoc IGsm + function DOMAIN_SEPARATOR() external view returns (bytes32) { + return _domainSeparatorV4(); + } + + /// @inheritdoc IGsm + function getGhoAmountForBuyAsset( + uint256 minAssetAmount + ) external view returns (uint256, uint256, uint256, uint256) { + return _calculateGhoAmountForBuyAsset(minAssetAmount); + } + + /// @inheritdoc IGsm + function getGhoAmountForSellAsset( + uint256 maxAssetAmount + ) external view returns (uint256, uint256, uint256, uint256) { + return _calculateGhoAmountForSellAsset(maxAssetAmount); + } + + /// @inheritdoc IGsm + function getAssetAmountForBuyAsset( + uint256 maxGhoAmount + ) external view returns (uint256, uint256, uint256, uint256) { + bool withFee = _feeStrategy != address(0); + uint256 grossAmount = withFee + ? IGsmFeeStrategy(_feeStrategy).getGrossAmountFromTotalBought(maxGhoAmount) + : maxGhoAmount; + // round down so maxGhoAmount is guaranteed + uint256 assetAmount = IGsmPriceStrategy(PRICE_STRATEGY).getGhoPriceInAsset(grossAmount, false); + uint256 finalGrossAmount = IGsmPriceStrategy(PRICE_STRATEGY).getAssetPriceInGho( + assetAmount, + true // TODO + ); + uint256 finalFee = withFee ? IGsmFeeStrategy(_feeStrategy).getBuyFee(finalGrossAmount) : 0; + return (assetAmount, finalGrossAmount + finalFee, finalGrossAmount, finalFee); + } + + /// @inheritdoc IGsm + function getAssetAmountForSellAsset( + uint256 minGhoAmount + ) external view returns (uint256, uint256, uint256, uint256) { + bool withFee = _feeStrategy != address(0); + uint256 grossAmount = withFee + ? IGsmFeeStrategy(_feeStrategy).getGrossAmountFromTotalSold(minGhoAmount) + : minGhoAmount; + // round up so minGhoAmount is guaranteed + uint256 assetAmount = IGsmPriceStrategy(PRICE_STRATEGY).getGhoPriceInAsset(grossAmount, true); + uint256 finalGrossAmount = IGsmPriceStrategy(PRICE_STRATEGY).getAssetPriceInGho( + assetAmount, + false // TODO + ); + uint256 finalFee = withFee ? IGsmFeeStrategy(_feeStrategy).getSellFee(finalGrossAmount) : 0; + return (assetAmount, finalGrossAmount - finalFee, finalGrossAmount, finalFee); + } + + /// @inheritdoc IGsm + function getAvailableUnderlyingExposure() external view returns (uint256) { + return _exposureCap > _currentExposure ? _exposureCap - _currentExposure : 0; + } + + /// @inheritdoc IGsm + function getAvailableLiquidity() external view returns (uint256) { + return _currentExposure; + } + + /// @inheritdoc IGsm + function getFeeStrategy() external view returns (address) { + return _feeStrategy; + } + + /// @inheritdoc IGsm + function getAccruedFees() external view returns (uint256) { + return _accruedFees; + } + + /// @inheritdoc IGsm + function getIsFrozen() external view returns (bool) { + return _isFrozen; + } + + /// @inheritdoc IGsm + function getIsSeized() external view returns (bool) { + return _isSeized; + } + + /// @inheritdoc IGsm + function canSwap() external view returns (bool) { + return !_isFrozen && !_isSeized; + } + + /// @inheritdoc IGhoFacilitator + function getGhoTreasury() external view override returns (address) { + return _ghoTreasury; + } + + /// @inheritdoc IGsm + function GSM_REVISION() public pure virtual override returns (uint256) { + return 1; + } + + /** + * @dev Buys an underlying asset with GHO + * @param originator The originator of the request + * @param minAmount The minimum amount of the underlying asset desired for purchase + * @param receiver The recipient address of the underlying asset being purchased + * @return The amount of underlying asset bought + * @return The amount of GHO sold by the user + */ + function _buyAsset( + address originator, + uint256 minAmount, + address receiver + ) internal returns (uint256, uint256) { + ( + uint256 assetAmount, + uint256 ghoSold, + uint256 grossAmount, + uint256 fee + ) = _calculateGhoAmountForBuyAsset(minAmount); + + _beforeBuyAsset(originator, assetAmount, receiver); + + require(assetAmount > 0, 'INVALID_AMOUNT'); + require(_currentExposure >= assetAmount, 'INSUFFICIENT_AVAILABLE_EXOGENOUS_ASSET_LIQUIDITY'); + + _currentExposure -= uint128(assetAmount); + _accruedFees += fee.toUint128(); + IGhoToken(GHO_TOKEN).transferFrom(originator, address(this), ghoSold); + IGhoToken(GHO_TOKEN).burn(grossAmount); + IERC20(UNDERLYING_ASSET).safeTransfer(receiver, assetAmount); + + emit BuyAsset(originator, receiver, assetAmount, ghoSold, fee); + return (assetAmount, ghoSold); + } + + /** + * @dev Hook that is called before `buyAsset`. + * @dev This can be used to add custom logic + * @param originator Originator of the request + * @param amount The amount of the underlying asset desired for purchase + * @param receiver Recipient address of the underlying asset being purchased + */ + function _beforeBuyAsset(address originator, uint256 amount, address receiver) internal virtual {} + + /** + * @dev Sells an underlying asset for GHO + * @param originator The originator of the request + * @param maxAmount The maximum amount of the underlying asset desired to sell + * @param receiver The recipient address of the GHO being purchased + * @return The amount of underlying asset sold + * @return The amount of GHO bought by the user + */ + function _sellAsset( + address originator, + uint256 maxAmount, + address receiver + ) internal returns (uint256, uint256) { + ( + uint256 assetAmount, + uint256 ghoBought, + uint256 grossAmount, + uint256 fee + ) = _calculateGhoAmountForSellAsset(maxAmount); + + _beforeSellAsset(originator, assetAmount, receiver); + + require(assetAmount > 0, 'INVALID_AMOUNT'); + require(_currentExposure + assetAmount <= _exposureCap, 'EXOGENOUS_ASSET_EXPOSURE_TOO_HIGH'); + + _currentExposure += uint128(assetAmount); + _accruedFees += fee.toUint128(); + IERC20(UNDERLYING_ASSET).safeTransferFrom(originator, address(this), assetAmount); + + IGhoToken(GHO_TOKEN).mint(address(this), grossAmount); + IGhoToken(GHO_TOKEN).transfer(receiver, ghoBought); + + emit SellAsset(originator, receiver, assetAmount, grossAmount, fee); + return (assetAmount, ghoBought); + } + + /** + * @dev Hook that is called before `sellAsset`. + * @dev This can be used to add custom logic + * @param originator Originator of the request + * @param amount The amount of the underlying asset desired to sell + * @param receiver Recipient address of the GHO being purchased + */ + function _beforeSellAsset( + address originator, + uint256 amount, + address receiver + ) internal virtual {} + + /** + * @dev Returns the amount of GHO sold in exchange of buying underlying asset + * @param assetAmount The amount of underlying asset to buy + * @return The exact amount of asset the user purchases + * @return The total amount of GHO the user sells (gross amount in GHO plus fee) + * @return The gross amount of GHO + * @return The fee amount in GHO, applied on top of gross amount of GHO + */ + function _calculateGhoAmountForBuyAsset( + uint256 assetAmount + ) internal view returns (uint256, uint256, uint256, uint256) { + bool withFee = _feeStrategy != address(0); + // pick the highest GHO amount possible for given asset amount + uint256 grossAmount = IGsmPriceStrategy(PRICE_STRATEGY).getAssetPriceInGho(assetAmount, true); + uint256 fee = withFee ? IGsmFeeStrategy(_feeStrategy).getBuyFee(grossAmount) : 0; + uint256 ghoSold = grossAmount + fee; + uint256 finalGrossAmount = withFee + ? IGsmFeeStrategy(_feeStrategy).getGrossAmountFromTotalBought(ghoSold) + : ghoSold; + // pick the lowest asset amount possible for given GHO amount + uint256 finalAssetAmount = IGsmPriceStrategy(PRICE_STRATEGY).getGhoPriceInAsset( + finalGrossAmount, + false + ); + uint256 finalFee = ghoSold - finalGrossAmount; + return (finalAssetAmount, finalGrossAmount + finalFee, finalGrossAmount, finalFee); + } + + /** + * @dev Returns the amount of GHO bought in exchange of a given amount of underlying asset + * @param assetAmount The amount of underlying asset to sell + * @return The exact amount of asset the user sells + * @return The total amount of GHO the user buys (gross amount in GHO minus fee) + * @return The gross amount of GHO + * @return The fee amount in GHO, applied to the gross amount of GHO + */ + function _calculateGhoAmountForSellAsset( + uint256 assetAmount + ) internal view returns (uint256, uint256, uint256, uint256) { + bool withFee = _feeStrategy != address(0); + // pick the lowest GHO amount possible for given asset amount + uint256 grossAmount = IGsmPriceStrategy(PRICE_STRATEGY).getAssetPriceInGho(assetAmount, false); + uint256 fee = withFee ? IGsmFeeStrategy(_feeStrategy).getSellFee(grossAmount) : 0; + uint256 ghoBought = grossAmount - fee; + uint256 finalGrossAmount = withFee + ? IGsmFeeStrategy(_feeStrategy).getGrossAmountFromTotalSold(ghoBought) + : ghoBought; + // pick the highest asset amount possible for given GHO amount + uint256 finalAssetAmount = IGsmPriceStrategy(PRICE_STRATEGY).getGhoPriceInAsset( + finalGrossAmount, + true + ); + uint256 finalFee = finalGrossAmount - ghoBought; + return (finalAssetAmount, finalGrossAmount - finalFee, finalGrossAmount, finalFee); + } + + /** + * @dev Updates Fee Strategy + * @param feeStrategy The address of the new Fee Strategy + */ + function _updateFeeStrategy(address feeStrategy) internal { + address oldFeeStrategy = _feeStrategy; + _feeStrategy = feeStrategy; + emit FeeStrategyUpdated(oldFeeStrategy, feeStrategy); + } + + /** + * @dev Updates Exposure Cap + * @param exposureCap The value of the new Exposure Cap + */ + function _updateExposureCap(uint128 exposureCap) internal { + uint128 oldExposureCap = _exposureCap; + _exposureCap = exposureCap; + emit ExposureCapUpdated(oldExposureCap, exposureCap); + } + + /** + * @dev Updates GHO Treasury Address + * @param newGhoTreasury The address of the new GHO Treasury + */ + function _updateGhoTreasury(address newGhoTreasury) internal { + require(newGhoTreasury != address(0), 'ZERO_ADDRESS_NOT_VALID'); + address oldGhoTreasury = _ghoTreasury; + _ghoTreasury = newGhoTreasury; + emit GhoTreasuryUpdated(oldGhoTreasury, newGhoTreasury); + } + + /// @inheritdoc VersionedInitializable + function getRevision() internal pure virtual override returns (uint256) { + return GSM_REVISION(); + } +} diff --git a/certora/GSM/mutations/mutants/Gsm/Gsm.sol3.sol b/certora/GSM/mutations/mutants/Gsm/Gsm.sol3.sol new file mode 100644 index 00000000..6364170b --- /dev/null +++ b/certora/GSM/mutations/mutants/Gsm/Gsm.sol3.sol @@ -0,0 +1,561 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.10; + +import {VersionedInitializable} from '@aave/core-v3/contracts/protocol/libraries/aave-upgradeability/VersionedInitializable.sol'; +import {IERC20} from '@aave/core-v3/contracts/dependencies/openzeppelin/contracts/IERC20.sol'; +import {GPv2SafeERC20} from '@aave/core-v3/contracts/dependencies/gnosis/contracts/GPv2SafeERC20.sol'; +import {EIP712} from '@openzeppelin/contracts/utils/cryptography/EIP712.sol'; +import {SignatureChecker} from '@openzeppelin/contracts/utils/cryptography/SignatureChecker.sol'; +import {SafeCast} from '@openzeppelin/contracts/utils/math/SafeCast.sol'; +import {AccessControl} from '@openzeppelin/contracts/access/AccessControl.sol'; +import {IGhoFacilitator} from '../../gho/interfaces/IGhoFacilitator.sol'; +import {IGhoToken} from '../../gho/interfaces/IGhoToken.sol'; +import {IGsmPriceStrategy} from './priceStrategy/interfaces/IGsmPriceStrategy.sol'; +import {IGsmFeeStrategy} from './feeStrategy/interfaces/IGsmFeeStrategy.sol'; +import {IGsm} from './interfaces/IGsm.sol'; + +/** + * @title Gsm + * @author Aave + * @notice GHO Stability Module. It provides buy/sell facilities to go to/from an underlying asset to/from GHO. + * @dev To be covered by a proxy contract. + */ +contract Gsm is AccessControl, VersionedInitializable, EIP712, IGsm { + using GPv2SafeERC20 for IERC20; + using SafeCast for uint256; + + /// @inheritdoc IGsm + bytes32 public constant CONFIGURATOR_ROLE = keccak256('CONFIGURATOR_ROLE'); + + /// @inheritdoc IGsm + bytes32 public constant TOKEN_RESCUER_ROLE = keccak256('TOKEN_RESCUER_ROLE'); + + /// @inheritdoc IGsm + bytes32 public constant SWAP_FREEZER_ROLE = keccak256('SWAP_FREEZER_ROLE'); + + /// @inheritdoc IGsm + bytes32 public constant LIQUIDATOR_ROLE = keccak256('LIQUIDATOR_ROLE'); + + /// @inheritdoc IGsm + bytes32 public constant BUY_ASSET_WITH_SIG_TYPEHASH = + keccak256( + 'BuyAssetWithSig(address originator,uint256 minAmount,address receiver,uint256 nonce,uint256 deadline)' + ); + + /// @inheritdoc IGsm + bytes32 public constant SELL_ASSET_WITH_SIG_TYPEHASH = + keccak256( + 'SellAssetWithSig(address originator,uint256 maxAmount,address receiver,uint256 nonce,uint256 deadline)' + ); + + /// @inheritdoc IGsm + address public immutable GHO_TOKEN; + + /// @inheritdoc IGsm + address public immutable UNDERLYING_ASSET; + + /// @inheritdoc IGsm + address public immutable PRICE_STRATEGY; + + /// @inheritdoc IGsm + mapping(address => uint256) public nonces; + + address internal _ghoTreasury; + address internal _feeStrategy; + bool internal _isFrozen; + bool internal _isSeized; + uint128 internal _exposureCap; + uint128 internal _currentExposure; + uint128 internal _accruedFees; + + /** + * @dev Require GSM to not be frozen for functions marked by this modifier + */ + modifier notFrozen() { + require(!_isFrozen, 'GSM_FROZEN'); + _; + } + + /** + * @dev Require GSM to not be seized for functions marked by this modifier + */ + modifier notSeized() { + /// SwapLinesMutation of: require(!_isSeized, 'GSM_SEIZED'); + _; + require(!_isSeized, 'GSM_SEIZED'); + } + + /** + * @dev Constructor + * @param ghoToken The address of the GHO token contract + * @param underlyingAsset The address of the collateral asset + * @param priceStrategy The address of the price strategy + */ + constructor(address ghoToken, address underlyingAsset, address priceStrategy) EIP712('GSM', '1') { + require(ghoToken != address(0), 'ZERO_ADDRESS_NOT_VALID'); + require(underlyingAsset != address(0), 'ZERO_ADDRESS_NOT_VALID'); + require( + IGsmPriceStrategy(priceStrategy).UNDERLYING_ASSET() == underlyingAsset, + 'INVALID_PRICE_STRATEGY' + ); + GHO_TOKEN = ghoToken; + UNDERLYING_ASSET = underlyingAsset; + PRICE_STRATEGY = priceStrategy; + } + + /** + * @notice GSM initializer + * @param admin The address of the default admin role + * @param ghoTreasury The address of the GHO treasury + * @param exposureCap Maximum amount of user-supplied underlying asset in GSM + */ + function initialize( + address admin, + address ghoTreasury, + uint128 exposureCap + ) external initializer { + require(admin != address(0), 'ZERO_ADDRESS_NOT_VALID'); + _grantRole(DEFAULT_ADMIN_ROLE, admin); + _grantRole(CONFIGURATOR_ROLE, admin); + _updateGhoTreasury(ghoTreasury); + _updateExposureCap(exposureCap); + } + + /// @inheritdoc IGsm + function buyAsset( + uint256 minAmount, + address receiver + ) external notFrozen notSeized returns (uint256, uint256) { + return _buyAsset(msg.sender, minAmount, receiver); + } + + /// @inheritdoc IGsm + function buyAssetWithSig( + address originator, + uint256 minAmount, + address receiver, + uint256 deadline, + bytes calldata signature + ) external notFrozen notSeized returns (uint256, uint256) { + require(deadline >= block.timestamp, 'SIGNATURE_DEADLINE_EXPIRED'); + bytes32 digest = keccak256( + abi.encode( + '\x19\x01', + _domainSeparatorV4(), + BUY_ASSET_WITH_SIG_TYPEHASH, + abi.encode(originator, minAmount, receiver, nonces[originator]++, deadline) + ) + ); + require( + SignatureChecker.isValidSignatureNow(originator, digest, signature), + 'SIGNATURE_INVALID' + ); + + return _buyAsset(originator, minAmount, receiver); + } + + /// @inheritdoc IGsm + function sellAsset( + uint256 maxAmount, + address receiver + ) external notFrozen notSeized returns (uint256, uint256) { + return _sellAsset(msg.sender, maxAmount, receiver); + } + + /// @inheritdoc IGsm + function sellAssetWithSig( + address originator, + uint256 maxAmount, + address receiver, + uint256 deadline, + bytes calldata signature + ) external notFrozen notSeized returns (uint256, uint256) { + require(deadline >= block.timestamp, 'SIGNATURE_DEADLINE_EXPIRED'); + bytes32 digest = keccak256( + abi.encode( + '\x19\x01', + _domainSeparatorV4(), + SELL_ASSET_WITH_SIG_TYPEHASH, + abi.encode(originator, maxAmount, receiver, nonces[originator]++, deadline) + ) + ); + require( + SignatureChecker.isValidSignatureNow(originator, digest, signature), + 'SIGNATURE_INVALID' + ); + + return _sellAsset(originator, maxAmount, receiver); + } + + /// @inheritdoc IGsm + function rescueTokens( + address token, + address to, + uint256 amount + ) external onlyRole(TOKEN_RESCUER_ROLE) { + require(amount > 0, 'INVALID_AMOUNT'); + if (token == GHO_TOKEN) { + uint256 rescuableBalance = IERC20(token).balanceOf(address(this)) - _accruedFees; + require(rescuableBalance >= amount, 'INSUFFICIENT_GHO_TO_RESCUE'); + } + if (token == UNDERLYING_ASSET) { + uint256 rescuableBalance = IERC20(token).balanceOf(address(this)) - _currentExposure; + require(rescuableBalance >= amount, 'INSUFFICIENT_EXOGENOUS_ASSET_TO_RESCUE'); + } + IERC20(token).safeTransfer(to, amount); + emit TokensRescued(token, to, amount); + } + + /// @inheritdoc IGsm + function setSwapFreeze(bool enable) external onlyRole(SWAP_FREEZER_ROLE) { + if (enable) { + require(!_isFrozen, 'GSM_ALREADY_FROZEN'); + } else { + require(_isFrozen, 'GSM_ALREADY_UNFROZEN'); + } + _isFrozen = enable; + emit SwapFreeze(msg.sender, enable); + } + + /// @inheritdoc IGsm + function seize() external notSeized onlyRole(LIQUIDATOR_ROLE) returns (uint256) { + _isSeized = true; + _currentExposure = 0; + _updateExposureCap(0); + + (, uint256 ghoMinted) = IGhoToken(GHO_TOKEN).getFacilitatorBucket(address(this)); + uint256 underlyingBalance = IERC20(UNDERLYING_ASSET).balanceOf(address(this)); + if (underlyingBalance > 0) { + IERC20(UNDERLYING_ASSET).safeTransfer(_ghoTreasury, underlyingBalance); + } + + emit Seized(msg.sender, _ghoTreasury, underlyingBalance, ghoMinted); + return underlyingBalance; + } + + /// @inheritdoc IGsm + function burnAfterSeize(uint256 amount) external onlyRole(LIQUIDATOR_ROLE) returns (uint256) { + require(_isSeized, 'GSM_NOT_SEIZED'); + require(amount > 0, 'INVALID_AMOUNT'); + + (, uint256 ghoMinted) = IGhoToken(GHO_TOKEN).getFacilitatorBucket(address(this)); + if (amount > ghoMinted) { + amount = ghoMinted; + } + IGhoToken(GHO_TOKEN).transferFrom(msg.sender, address(this), amount); + IGhoToken(GHO_TOKEN).burn(amount); + + emit BurnAfterSeize(msg.sender, amount, (ghoMinted - amount)); + return amount; + } + + /// @inheritdoc IGsm + function updateFeeStrategy(address feeStrategy) external onlyRole(CONFIGURATOR_ROLE) { + _updateFeeStrategy(feeStrategy); + } + + /// @inheritdoc IGsm + function updateExposureCap(uint128 exposureCap) external onlyRole(CONFIGURATOR_ROLE) { + _updateExposureCap(exposureCap); + } + + /// @inheritdoc IGhoFacilitator + function distributeFeesToTreasury() public virtual override { + uint256 accruedFees = _accruedFees; + if (accruedFees > 0) { + _accruedFees = 0; + IERC20(GHO_TOKEN).transfer(_ghoTreasury, accruedFees); + emit FeesDistributedToTreasury(_ghoTreasury, GHO_TOKEN, accruedFees); + } + } + + /// @inheritdoc IGhoFacilitator + function updateGhoTreasury(address newGhoTreasury) external override onlyRole(CONFIGURATOR_ROLE) { + _updateGhoTreasury(newGhoTreasury); + } + + /// @inheritdoc IGsm + function DOMAIN_SEPARATOR() external view returns (bytes32) { + return _domainSeparatorV4(); + } + + /// @inheritdoc IGsm + function getGhoAmountForBuyAsset( + uint256 minAssetAmount + ) external view returns (uint256, uint256, uint256, uint256) { + return _calculateGhoAmountForBuyAsset(minAssetAmount); + } + + /// @inheritdoc IGsm + function getGhoAmountForSellAsset( + uint256 maxAssetAmount + ) external view returns (uint256, uint256, uint256, uint256) { + return _calculateGhoAmountForSellAsset(maxAssetAmount); + } + + /// @inheritdoc IGsm + function getAssetAmountForBuyAsset( + uint256 maxGhoAmount + ) external view returns (uint256, uint256, uint256, uint256) { + bool withFee = _feeStrategy != address(0); + uint256 grossAmount = withFee + ? IGsmFeeStrategy(_feeStrategy).getGrossAmountFromTotalBought(maxGhoAmount) + : maxGhoAmount; + // round down so maxGhoAmount is guaranteed + uint256 assetAmount = IGsmPriceStrategy(PRICE_STRATEGY).getGhoPriceInAsset(grossAmount, false); + uint256 finalGrossAmount = IGsmPriceStrategy(PRICE_STRATEGY).getAssetPriceInGho( + assetAmount, + true // TODO + ); + uint256 finalFee = withFee ? IGsmFeeStrategy(_feeStrategy).getBuyFee(finalGrossAmount) : 0; + return (assetAmount, finalGrossAmount + finalFee, finalGrossAmount, finalFee); + } + + /// @inheritdoc IGsm + function getAssetAmountForSellAsset( + uint256 minGhoAmount + ) external view returns (uint256, uint256, uint256, uint256) { + bool withFee = _feeStrategy != address(0); + uint256 grossAmount = withFee + ? IGsmFeeStrategy(_feeStrategy).getGrossAmountFromTotalSold(minGhoAmount) + : minGhoAmount; + // round up so minGhoAmount is guaranteed + uint256 assetAmount = IGsmPriceStrategy(PRICE_STRATEGY).getGhoPriceInAsset(grossAmount, true); + uint256 finalGrossAmount = IGsmPriceStrategy(PRICE_STRATEGY).getAssetPriceInGho( + assetAmount, + false // TODO + ); + uint256 finalFee = withFee ? IGsmFeeStrategy(_feeStrategy).getSellFee(finalGrossAmount) : 0; + return (assetAmount, finalGrossAmount - finalFee, finalGrossAmount, finalFee); + } + + /// @inheritdoc IGsm + function getAvailableUnderlyingExposure() external view returns (uint256) { + return _exposureCap > _currentExposure ? _exposureCap - _currentExposure : 0; + } + + /// @inheritdoc IGsm + function getAvailableLiquidity() external view returns (uint256) { + return _currentExposure; + } + + /// @inheritdoc IGsm + function getFeeStrategy() external view returns (address) { + return _feeStrategy; + } + + /// @inheritdoc IGsm + function getAccruedFees() external view returns (uint256) { + return _accruedFees; + } + + /// @inheritdoc IGsm + function getIsFrozen() external view returns (bool) { + return _isFrozen; + } + + /// @inheritdoc IGsm + function getIsSeized() external view returns (bool) { + return _isSeized; + } + + /// @inheritdoc IGsm + function canSwap() external view returns (bool) { + return !_isFrozen && !_isSeized; + } + + /// @inheritdoc IGhoFacilitator + function getGhoTreasury() external view override returns (address) { + return _ghoTreasury; + } + + /// @inheritdoc IGsm + function GSM_REVISION() public pure virtual override returns (uint256) { + return 1; + } + + /** + * @dev Buys an underlying asset with GHO + * @param originator The originator of the request + * @param minAmount The minimum amount of the underlying asset desired for purchase + * @param receiver The recipient address of the underlying asset being purchased + * @return The amount of underlying asset bought + * @return The amount of GHO sold by the user + */ + function _buyAsset( + address originator, + uint256 minAmount, + address receiver + ) internal returns (uint256, uint256) { + ( + uint256 assetAmount, + uint256 ghoSold, + uint256 grossAmount, + uint256 fee + ) = _calculateGhoAmountForBuyAsset(minAmount); + + _beforeBuyAsset(originator, assetAmount, receiver); + + require(assetAmount > 0, 'INVALID_AMOUNT'); + require(_currentExposure >= assetAmount, 'INSUFFICIENT_AVAILABLE_EXOGENOUS_ASSET_LIQUIDITY'); + + _currentExposure -= uint128(assetAmount); + _accruedFees += fee.toUint128(); + IGhoToken(GHO_TOKEN).transferFrom(originator, address(this), ghoSold); + IGhoToken(GHO_TOKEN).burn(grossAmount); + IERC20(UNDERLYING_ASSET).safeTransfer(receiver, assetAmount); + + emit BuyAsset(originator, receiver, assetAmount, ghoSold, fee); + return (assetAmount, ghoSold); + } + + /** + * @dev Hook that is called before `buyAsset`. + * @dev This can be used to add custom logic + * @param originator Originator of the request + * @param amount The amount of the underlying asset desired for purchase + * @param receiver Recipient address of the underlying asset being purchased + */ + function _beforeBuyAsset(address originator, uint256 amount, address receiver) internal virtual {} + + /** + * @dev Sells an underlying asset for GHO + * @param originator The originator of the request + * @param maxAmount The maximum amount of the underlying asset desired to sell + * @param receiver The recipient address of the GHO being purchased + * @return The amount of underlying asset sold + * @return The amount of GHO bought by the user + */ + function _sellAsset( + address originator, + uint256 maxAmount, + address receiver + ) internal returns (uint256, uint256) { + ( + uint256 assetAmount, + uint256 ghoBought, + uint256 grossAmount, + uint256 fee + ) = _calculateGhoAmountForSellAsset(maxAmount); + + _beforeSellAsset(originator, assetAmount, receiver); + + require(assetAmount > 0, 'INVALID_AMOUNT'); + require(_currentExposure + assetAmount <= _exposureCap, 'EXOGENOUS_ASSET_EXPOSURE_TOO_HIGH'); + + _currentExposure += uint128(assetAmount); + _accruedFees += fee.toUint128(); + IERC20(UNDERLYING_ASSET).safeTransferFrom(originator, address(this), assetAmount); + + IGhoToken(GHO_TOKEN).mint(address(this), grossAmount); + IGhoToken(GHO_TOKEN).transfer(receiver, ghoBought); + + emit SellAsset(originator, receiver, assetAmount, grossAmount, fee); + return (assetAmount, ghoBought); + } + + /** + * @dev Hook that is called before `sellAsset`. + * @dev This can be used to add custom logic + * @param originator Originator of the request + * @param amount The amount of the underlying asset desired to sell + * @param receiver Recipient address of the GHO being purchased + */ + function _beforeSellAsset( + address originator, + uint256 amount, + address receiver + ) internal virtual {} + + /** + * @dev Returns the amount of GHO sold in exchange of buying underlying asset + * @param assetAmount The amount of underlying asset to buy + * @return The exact amount of asset the user purchases + * @return The total amount of GHO the user sells (gross amount in GHO plus fee) + * @return The gross amount of GHO + * @return The fee amount in GHO, applied on top of gross amount of GHO + */ + function _calculateGhoAmountForBuyAsset( + uint256 assetAmount + ) internal view returns (uint256, uint256, uint256, uint256) { + bool withFee = _feeStrategy != address(0); + // pick the highest GHO amount possible for given asset amount + uint256 grossAmount = IGsmPriceStrategy(PRICE_STRATEGY).getAssetPriceInGho(assetAmount, true); + uint256 fee = withFee ? IGsmFeeStrategy(_feeStrategy).getBuyFee(grossAmount) : 0; + uint256 ghoSold = grossAmount + fee; + uint256 finalGrossAmount = withFee + ? IGsmFeeStrategy(_feeStrategy).getGrossAmountFromTotalBought(ghoSold) + : ghoSold; + // pick the lowest asset amount possible for given GHO amount + uint256 finalAssetAmount = IGsmPriceStrategy(PRICE_STRATEGY).getGhoPriceInAsset( + finalGrossAmount, + false + ); + uint256 finalFee = ghoSold - finalGrossAmount; + return (finalAssetAmount, finalGrossAmount + finalFee, finalGrossAmount, finalFee); + } + + /** + * @dev Returns the amount of GHO bought in exchange of a given amount of underlying asset + * @param assetAmount The amount of underlying asset to sell + * @return The exact amount of asset the user sells + * @return The total amount of GHO the user buys (gross amount in GHO minus fee) + * @return The gross amount of GHO + * @return The fee amount in GHO, applied to the gross amount of GHO + */ + function _calculateGhoAmountForSellAsset( + uint256 assetAmount + ) internal view returns (uint256, uint256, uint256, uint256) { + bool withFee = _feeStrategy != address(0); + // pick the lowest GHO amount possible for given asset amount + uint256 grossAmount = IGsmPriceStrategy(PRICE_STRATEGY).getAssetPriceInGho(assetAmount, false); + uint256 fee = withFee ? IGsmFeeStrategy(_feeStrategy).getSellFee(grossAmount) : 0; + uint256 ghoBought = grossAmount - fee; + uint256 finalGrossAmount = withFee + ? IGsmFeeStrategy(_feeStrategy).getGrossAmountFromTotalSold(ghoBought) + : ghoBought; + // pick the highest asset amount possible for given GHO amount + uint256 finalAssetAmount = IGsmPriceStrategy(PRICE_STRATEGY).getGhoPriceInAsset( + finalGrossAmount, + true + ); + uint256 finalFee = finalGrossAmount - ghoBought; + return (finalAssetAmount, finalGrossAmount - finalFee, finalGrossAmount, finalFee); + } + + /** + * @dev Updates Fee Strategy + * @param feeStrategy The address of the new Fee Strategy + */ + function _updateFeeStrategy(address feeStrategy) internal { + address oldFeeStrategy = _feeStrategy; + _feeStrategy = feeStrategy; + emit FeeStrategyUpdated(oldFeeStrategy, feeStrategy); + } + + /** + * @dev Updates Exposure Cap + * @param exposureCap The value of the new Exposure Cap + */ + function _updateExposureCap(uint128 exposureCap) internal { + uint128 oldExposureCap = _exposureCap; + _exposureCap = exposureCap; + emit ExposureCapUpdated(oldExposureCap, exposureCap); + } + + /** + * @dev Updates GHO Treasury Address + * @param newGhoTreasury The address of the new GHO Treasury + */ + function _updateGhoTreasury(address newGhoTreasury) internal { + require(newGhoTreasury != address(0), 'ZERO_ADDRESS_NOT_VALID'); + address oldGhoTreasury = _ghoTreasury; + _ghoTreasury = newGhoTreasury; + emit GhoTreasuryUpdated(oldGhoTreasury, newGhoTreasury); + } + + /// @inheritdoc VersionedInitializable + function getRevision() internal pure virtual override returns (uint256) { + return GSM_REVISION(); + } +} diff --git a/certora/GSM/mutations/mutants/feeStrategy/FixedFeeStrategy.sol14.sol b/certora/GSM/mutations/mutants/feeStrategy/FixedFeeStrategy.sol14.sol new file mode 100644 index 00000000..067cecc0 --- /dev/null +++ b/certora/GSM/mutations/mutants/feeStrategy/FixedFeeStrategy.sol14.sol @@ -0,0 +1,71 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.10; + +import {Math} from '@openzeppelin/contracts/utils/math/Math.sol'; +import {PercentageMath} from '@aave/core-v3/contracts/protocol/libraries/math/PercentageMath.sol'; +import {IGsmFeeStrategy} from './interfaces/IGsmFeeStrategy.sol'; + +/** + * @title FixedFeeStrategy + * @author Aave + * @notice Fee strategy using a fixed rate to calculate buy/sell fees + */ +contract FixedFeeStrategy is IGsmFeeStrategy { + using Math for uint256; + + uint256 internal immutable _buyFee; + uint256 internal immutable _sellFee; + + /** + * @dev Constructor + * @dev Fees must be lower than 5000 bps (e.g. 50.00%) + * @param buyFee The fee paid when buying the underlying asset in exchange for GHO, expressed in bps + * @param sellFee The fee paid when selling the underlying asset in exchange for GHO, expressed in bps + */ + constructor(uint256 buyFee, uint256 sellFee) { + require(buyFee < 5000, 'INVALID_BUY_FEE'); + require(sellFee < 5000, 'INVALID_SELL_FEE'); + require(buyFee > 0 || sellFee > 0, 'MUST_HAVE_ONE_NONZERO_FEE'); + _buyFee = buyFee; + _sellFee = sellFee; + } + + /// @inheritdoc IGsmFeeStrategy + function getBuyFee(uint256 grossAmount) external view returns (uint256) { + return grossAmount.mulDiv(_buyFee, PercentageMath.PERCENTAGE_FACTOR, Math.Rounding.Up); + } + + /// @inheritdoc IGsmFeeStrategy + function getSellFee(uint256 grossAmount) external view returns (uint256) { + return grossAmount.mulDiv(_sellFee, PercentageMath.PERCENTAGE_FACTOR, Math.Rounding.Up); + } + + /// @inheritdoc IGsmFeeStrategy + function getGrossAmountFromTotalBought(uint256 totalAmount) external view returns (uint256) { + if (totalAmount == 0) { + return 0; + } else if (_buyFee == 0) { + return totalAmount; + } else { + return + /// FunctionCallMutation of: totalAmount.mulDiv( + PercentageMath.PERCENTAGE_FACTOR; + } + } + + /// @inheritdoc IGsmFeeStrategy + function getGrossAmountFromTotalSold(uint256 totalAmount) external view returns (uint256) { + if (totalAmount == 0) { + return 0; + } else if (_sellFee == 0) { + return totalAmount; + } else { + return + totalAmount.mulDiv( + PercentageMath.PERCENTAGE_FACTOR, + PercentageMath.PERCENTAGE_FACTOR - _sellFee, + Math.Rounding.Up + ); + } + } +} diff --git a/certora/GSM/mutations/mutants/feeStrategy/FixedFeeStrategy.sol16.sol b/certora/GSM/mutations/mutants/feeStrategy/FixedFeeStrategy.sol16.sol new file mode 100644 index 00000000..9c53839f --- /dev/null +++ b/certora/GSM/mutations/mutants/feeStrategy/FixedFeeStrategy.sol16.sol @@ -0,0 +1,75 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.10; + +import {Math} from '@openzeppelin/contracts/utils/math/Math.sol'; +import {PercentageMath} from '@aave/core-v3/contracts/protocol/libraries/math/PercentageMath.sol'; +import {IGsmFeeStrategy} from './interfaces/IGsmFeeStrategy.sol'; + +/** + * @title FixedFeeStrategy + * @author Aave + * @notice Fee strategy using a fixed rate to calculate buy/sell fees + */ +contract FixedFeeStrategy is IGsmFeeStrategy { + using Math for uint256; + + uint256 internal immutable _buyFee; + uint256 internal immutable _sellFee; + + /** + * @dev Constructor + * @dev Fees must be lower than 5000 bps (e.g. 50.00%) + * @param buyFee The fee paid when buying the underlying asset in exchange for GHO, expressed in bps + * @param sellFee The fee paid when selling the underlying asset in exchange for GHO, expressed in bps + */ + constructor(uint256 buyFee, uint256 sellFee) { + require(buyFee < 5000, 'INVALID_BUY_FEE'); + require(sellFee < 5000, 'INVALID_SELL_FEE'); + require(buyFee > 0 || sellFee > 0, 'MUST_HAVE_ONE_NONZERO_FEE'); + _buyFee = buyFee; + _sellFee = sellFee; + } + + /// @inheritdoc IGsmFeeStrategy + function getBuyFee(uint256 grossAmount) external view returns (uint256) { + return grossAmount.mulDiv(_buyFee, PercentageMath.PERCENTAGE_FACTOR, Math.Rounding.Up); + } + + /// @inheritdoc IGsmFeeStrategy + function getSellFee(uint256 grossAmount) external view returns (uint256) { + return grossAmount.mulDiv(_sellFee, PercentageMath.PERCENTAGE_FACTOR, Math.Rounding.Up); + } + + /// @inheritdoc IGsmFeeStrategy + function getGrossAmountFromTotalBought(uint256 totalAmount) external view returns (uint256) { + if (totalAmount == 0) { + return 0; + } else if (_buyFee == 0) { + return totalAmount; + } else { + return + totalAmount.mulDiv( + PercentageMath.PERCENTAGE_FACTOR, + /// BinaryOpMutation of: PercentageMath.PERCENTAGE_FACTOR + _buyFee, + PercentageMath.PERCENTAGE_FACTOR / _buyFee, + Math.Rounding.Down + ); + } + } + + /// @inheritdoc IGsmFeeStrategy + function getGrossAmountFromTotalSold(uint256 totalAmount) external view returns (uint256) { + if (totalAmount == 0) { + return 0; + } else if (_sellFee == 0) { + return totalAmount; + } else { + return + totalAmount.mulDiv( + PercentageMath.PERCENTAGE_FACTOR, + PercentageMath.PERCENTAGE_FACTOR - _sellFee, + Math.Rounding.Up + ); + } + } +} diff --git a/certora/GSM/mutations/mutants/feeStrategy/FixedFeeStrategy.sol17.sol b/certora/GSM/mutations/mutants/feeStrategy/FixedFeeStrategy.sol17.sol new file mode 100644 index 00000000..b20407e4 --- /dev/null +++ b/certora/GSM/mutations/mutants/feeStrategy/FixedFeeStrategy.sol17.sol @@ -0,0 +1,75 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.10; + +import {Math} from '@openzeppelin/contracts/utils/math/Math.sol'; +import {PercentageMath} from '@aave/core-v3/contracts/protocol/libraries/math/PercentageMath.sol'; +import {IGsmFeeStrategy} from './interfaces/IGsmFeeStrategy.sol'; + +/** + * @title FixedFeeStrategy + * @author Aave + * @notice Fee strategy using a fixed rate to calculate buy/sell fees + */ +contract FixedFeeStrategy is IGsmFeeStrategy { + using Math for uint256; + + uint256 internal immutable _buyFee; + uint256 internal immutable _sellFee; + + /** + * @dev Constructor + * @dev Fees must be lower than 5000 bps (e.g. 50.00%) + * @param buyFee The fee paid when buying the underlying asset in exchange for GHO, expressed in bps + * @param sellFee The fee paid when selling the underlying asset in exchange for GHO, expressed in bps + */ + constructor(uint256 buyFee, uint256 sellFee) { + require(buyFee < 5000, 'INVALID_BUY_FEE'); + require(sellFee < 5000, 'INVALID_SELL_FEE'); + require(buyFee > 0 || sellFee > 0, 'MUST_HAVE_ONE_NONZERO_FEE'); + _buyFee = buyFee; + _sellFee = sellFee; + } + + /// @inheritdoc IGsmFeeStrategy + function getBuyFee(uint256 grossAmount) external view returns (uint256) { + return grossAmount.mulDiv(_buyFee, PercentageMath.PERCENTAGE_FACTOR, Math.Rounding.Up); + } + + /// @inheritdoc IGsmFeeStrategy + function getSellFee(uint256 grossAmount) external view returns (uint256) { + return grossAmount.mulDiv(_sellFee, PercentageMath.PERCENTAGE_FACTOR, Math.Rounding.Up); + } + + /// @inheritdoc IGsmFeeStrategy + function getGrossAmountFromTotalBought(uint256 totalAmount) external view returns (uint256) { + /// IfStatementMutation of: if (totalAmount == 0) { + if (!(totalAmount == 0)) { + return 0; + } else if (_buyFee == 0) { + return totalAmount; + } else { + return + totalAmount.mulDiv( + PercentageMath.PERCENTAGE_FACTOR, + PercentageMath.PERCENTAGE_FACTOR + _buyFee, + Math.Rounding.Down + ); + } + } + + /// @inheritdoc IGsmFeeStrategy + function getGrossAmountFromTotalSold(uint256 totalAmount) external view returns (uint256) { + if (totalAmount == 0) { + return 0; + } else if (_sellFee == 0) { + return totalAmount; + } else { + return + totalAmount.mulDiv( + PercentageMath.PERCENTAGE_FACTOR, + PercentageMath.PERCENTAGE_FACTOR - _sellFee, + Math.Rounding.Up + ); + } + } +} diff --git a/certora/GSM/mutations/mutants/feeStrategy/FixedFeeStrategy.sol9.sol b/certora/GSM/mutations/mutants/feeStrategy/FixedFeeStrategy.sol9.sol new file mode 100644 index 00000000..4fcc248a --- /dev/null +++ b/certora/GSM/mutations/mutants/feeStrategy/FixedFeeStrategy.sol9.sol @@ -0,0 +1,75 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.10; + +import {Math} from '@openzeppelin/contracts/utils/math/Math.sol'; +import {PercentageMath} from '@aave/core-v3/contracts/protocol/libraries/math/PercentageMath.sol'; +import {IGsmFeeStrategy} from './interfaces/IGsmFeeStrategy.sol'; + +/** + * @title FixedFeeStrategy + * @author Aave + * @notice Fee strategy using a fixed rate to calculate buy/sell fees + */ +contract FixedFeeStrategy is IGsmFeeStrategy { + using Math for uint256; + + uint256 internal immutable _buyFee; + uint256 internal immutable _sellFee; + + /** + * @dev Constructor + * @dev Fees must be lower than 5000 bps (e.g. 50.00%) + * @param buyFee The fee paid when buying the underlying asset in exchange for GHO, expressed in bps + * @param sellFee The fee paid when selling the underlying asset in exchange for GHO, expressed in bps + */ + constructor(uint256 buyFee, uint256 sellFee) { + require(buyFee < 5000, 'INVALID_BUY_FEE'); + require(sellFee < 5000, 'INVALID_SELL_FEE'); + require(buyFee > 0 || sellFee > 0, 'MUST_HAVE_ONE_NONZERO_FEE'); + _buyFee = buyFee; + _sellFee = sellFee; + } + + /// @inheritdoc IGsmFeeStrategy + function getBuyFee(uint256 grossAmount) external view returns (uint256) { + return grossAmount.mulDiv(_buyFee, PercentageMath.PERCENTAGE_FACTOR, Math.Rounding.Up); + } + + /// @inheritdoc IGsmFeeStrategy + function getSellFee(uint256 grossAmount) external view returns (uint256) { + return grossAmount.mulDiv(_sellFee, PercentageMath.PERCENTAGE_FACTOR, Math.Rounding.Up); + } + + /// @inheritdoc IGsmFeeStrategy + function getGrossAmountFromTotalBought(uint256 totalAmount) external view returns (uint256) { + if (totalAmount == 0) { + return 0; + } else if (_buyFee == 0) { + return totalAmount; + } else { + return + totalAmount.mulDiv( + PercentageMath.PERCENTAGE_FACTOR, + PercentageMath.PERCENTAGE_FACTOR + _buyFee, + Math.Rounding.Down + ); + } + } + + /// @inheritdoc IGsmFeeStrategy + function getGrossAmountFromTotalSold(uint256 totalAmount) external view returns (uint256) { + if (totalAmount == 0) { + return 0; + } else if (_sellFee == 0) { + return totalAmount; + } else { + return + totalAmount.mulDiv( + PercentageMath.PERCENTAGE_FACTOR, + /// BinaryOpMutation of: PercentageMath.PERCENTAGE_FACTOR - _sellFee, + PercentageMath.PERCENTAGE_FACTOR + _sellFee, + Math.Rounding.Up + ); + } + } +} diff --git a/certora/GSM/mutations/mutants/priceStrategy/FixedPriceStrategy.sol10 copy 2.sol b/certora/GSM/mutations/mutants/priceStrategy/FixedPriceStrategy.sol10 copy 2.sol new file mode 100644 index 00000000..78d69291 --- /dev/null +++ b/certora/GSM/mutations/mutants/priceStrategy/FixedPriceStrategy.sol10 copy 2.sol @@ -0,0 +1,64 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.10; + +import {Math} from '@openzeppelin/contracts/utils/math/Math.sol'; +import {IGsmPriceStrategy} from './interfaces/IGsmPriceStrategy.sol'; + +/** + * @title FixedPriceStrategy + * @author Aave + * @notice Price strategy involving a fixed-rate conversion from an underlying asset to GHO + */ +contract FixedPriceStrategy is IGsmPriceStrategy { + using Math for uint256; + + /// @inheritdoc IGsmPriceStrategy + uint256 public constant GHO_DECIMALS = 18; + + /// @inheritdoc IGsmPriceStrategy + address public immutable UNDERLYING_ASSET; + + /// @inheritdoc IGsmPriceStrategy + uint256 public immutable UNDERLYING_ASSET_DECIMALS; + + /// @dev The price ratio from underlying asset to GHO (expressed in WAD), e.g. a ratio of 2e18 means 2 GHO per 1 underlying asset + uint256 public immutable PRICE_RATIO; + + /// @dev Underlying asset units represent units for the underlying asset + uint256 internal immutable _underlyingAssetUnits; + + /** + * @dev Constructor + * @param priceRatio The price ratio from underlying asset to GHO (expressed in WAD) + * @param underlyingAsset The address of the underlying asset + * @param underlyingAssetDecimals The number of decimals of the underlying asset + */ + constructor(uint256 priceRatio, address underlyingAsset, uint8 underlyingAssetDecimals) { + require(priceRatio > 0, 'INVALID_PRICE_RATIO'); + PRICE_RATIO = priceRatio; + UNDERLYING_ASSET = underlyingAsset; + UNDERLYING_ASSET_DECIMALS = underlyingAssetDecimals; + /// AssignmentMutation of: _underlyingAssetUnits = 10 ** underlyingAssetDecimals; + _underlyingAssetUnits = 1; + } + + /// @inheritdoc IGsmPriceStrategy + function getAssetPriceInGho(uint256 assetAmount, bool roundUp) external view returns (uint256) { + return + assetAmount.mulDiv( + PRICE_RATIO, + _underlyingAssetUnits, + roundUp ? Math.Rounding.Up : Math.Rounding.Down + ); + } + + /// @inheritdoc IGsmPriceStrategy + function getGhoPriceInAsset(uint256 ghoAmount, bool roundUp) external view returns (uint256) { + return + ghoAmount.mulDiv( + _underlyingAssetUnits, + PRICE_RATIO, + roundUp ? Math.Rounding.Up : Math.Rounding.Down + ); + } +} diff --git a/certora/GSM/mutations/mutants/priceStrategy/FixedPriceStrategy.sol10 copy.sol b/certora/GSM/mutations/mutants/priceStrategy/FixedPriceStrategy.sol10 copy.sol new file mode 100644 index 00000000..31ae00ed --- /dev/null +++ b/certora/GSM/mutations/mutants/priceStrategy/FixedPriceStrategy.sol10 copy.sol @@ -0,0 +1,64 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.10; + +import {Math} from '@openzeppelin/contracts/utils/math/Math.sol'; +import {IGsmPriceStrategy} from './interfaces/IGsmPriceStrategy.sol'; + +/** + * @title FixedPriceStrategy + * @author Aave + * @notice Price strategy involving a fixed-rate conversion from an underlying asset to GHO + */ +contract FixedPriceStrategy is IGsmPriceStrategy { + using Math for uint256; + + /// @inheritdoc IGsmPriceStrategy + uint256 public constant GHO_DECIMALS = 18; + + /// @inheritdoc IGsmPriceStrategy + address public immutable UNDERLYING_ASSET; + + /// @inheritdoc IGsmPriceStrategy + uint256 public immutable UNDERLYING_ASSET_DECIMALS; + + /// @dev The price ratio from underlying asset to GHO (expressed in WAD), e.g. a ratio of 2e18 means 2 GHO per 1 underlying asset + uint256 public immutable PRICE_RATIO; + + /// @dev Underlying asset units represent units for the underlying asset + uint256 internal immutable _underlyingAssetUnits; + + /** + * @dev Constructor + * @param priceRatio The price ratio from underlying asset to GHO (expressed in WAD) + * @param underlyingAsset The address of the underlying asset + * @param underlyingAssetDecimals The number of decimals of the underlying asset + */ + constructor(uint256 priceRatio, address underlyingAsset, uint8 underlyingAssetDecimals) { + require(priceRatio > 0, 'INVALID_PRICE_RATIO'); + /// AssignmentMutation of: PRICE_RATIO = priceRatio; + PRICE_RATIO = 1; + UNDERLYING_ASSET = underlyingAsset; + UNDERLYING_ASSET_DECIMALS = underlyingAssetDecimals; + _underlyingAssetUnits = 10 ** underlyingAssetDecimals; + } + + /// @inheritdoc IGsmPriceStrategy + function getAssetPriceInGho(uint256 assetAmount, bool roundUp) external view returns (uint256) { + return + assetAmount.mulDiv( + PRICE_RATIO, + _underlyingAssetUnits, + roundUp ? Math.Rounding.Up : Math.Rounding.Down + ); + } + + /// @inheritdoc IGsmPriceStrategy + function getGhoPriceInAsset(uint256 ghoAmount, bool roundUp) external view returns (uint256) { + return + ghoAmount.mulDiv( + _underlyingAssetUnits, + PRICE_RATIO, + roundUp ? Math.Rounding.Up : Math.Rounding.Down + ); + } +} diff --git a/certora/GSM/mutations/mutants/priceStrategy/FixedPriceStrategy.sol10.sol b/certora/GSM/mutations/mutants/priceStrategy/FixedPriceStrategy.sol10.sol new file mode 100644 index 00000000..30cc05a4 --- /dev/null +++ b/certora/GSM/mutations/mutants/priceStrategy/FixedPriceStrategy.sol10.sol @@ -0,0 +1,64 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.10; + +import {Math} from '@openzeppelin/contracts/utils/math/Math.sol'; +import {IGsmPriceStrategy} from './interfaces/IGsmPriceStrategy.sol'; + +/** + * @title FixedPriceStrategy + * @author Aave + * @notice Price strategy involving a fixed-rate conversion from an underlying asset to GHO + */ +contract FixedPriceStrategy is IGsmPriceStrategy { + using Math for uint256; + + /// @inheritdoc IGsmPriceStrategy + uint256 public constant GHO_DECIMALS = 18; + + /// @inheritdoc IGsmPriceStrategy + address public immutable UNDERLYING_ASSET; + + /// @inheritdoc IGsmPriceStrategy + uint256 public immutable UNDERLYING_ASSET_DECIMALS; + + /// @dev The price ratio from underlying asset to GHO (expressed in WAD), e.g. a ratio of 2e18 means 2 GHO per 1 underlying asset + uint256 public immutable PRICE_RATIO; + + /// @dev Underlying asset units represent units for the underlying asset + uint256 internal immutable _underlyingAssetUnits; + + /** + * @dev Constructor + * @param priceRatio The price ratio from underlying asset to GHO (expressed in WAD) + * @param underlyingAsset The address of the underlying asset + * @param underlyingAssetDecimals The number of decimals of the underlying asset + */ + constructor(uint256 priceRatio, address underlyingAsset, uint8 underlyingAssetDecimals) { + require(priceRatio > 0, 'INVALID_PRICE_RATIO'); + PRICE_RATIO = priceRatio; + UNDERLYING_ASSET = underlyingAsset; + /// AssignmentMutation of: UNDERLYING_ASSET_DECIMALS = underlyingAssetDecimals; + UNDERLYING_ASSET_DECIMALS = 1; + _underlyingAssetUnits = 10 ** underlyingAssetDecimals; + } + + /// @inheritdoc IGsmPriceStrategy + function getAssetPriceInGho(uint256 assetAmount, bool roundUp) external view returns (uint256) { + return + assetAmount.mulDiv( + PRICE_RATIO, + _underlyingAssetUnits, + roundUp ? Math.Rounding.Up : Math.Rounding.Down + ); + } + + /// @inheritdoc IGsmPriceStrategy + function getGhoPriceInAsset(uint256 ghoAmount, bool roundUp) external view returns (uint256) { + return + ghoAmount.mulDiv( + _underlyingAssetUnits, + PRICE_RATIO, + roundUp ? Math.Rounding.Up : Math.Rounding.Down + ); + } +} diff --git a/certora/GSM/mutations/mutants/priceStrategy/FixedPriceStrategy.sol12.sol b/certora/GSM/mutations/mutants/priceStrategy/FixedPriceStrategy.sol12.sol new file mode 100644 index 00000000..7d568002 --- /dev/null +++ b/certora/GSM/mutations/mutants/priceStrategy/FixedPriceStrategy.sol12.sol @@ -0,0 +1,64 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.10; + +import {Math} from '@openzeppelin/contracts/utils/math/Math.sol'; +import {IGsmPriceStrategy} from './interfaces/IGsmPriceStrategy.sol'; + +/** + * @title FixedPriceStrategy + * @author Aave + * @notice Price strategy involving a fixed-rate conversion from an underlying asset to GHO + */ +contract FixedPriceStrategy is IGsmPriceStrategy { + using Math for uint256; + + /// @inheritdoc IGsmPriceStrategy + uint256 public constant GHO_DECIMALS = 18; + + /// @inheritdoc IGsmPriceStrategy + address public immutable UNDERLYING_ASSET; + + /// @inheritdoc IGsmPriceStrategy + uint256 public immutable UNDERLYING_ASSET_DECIMALS; + + /// @dev The price ratio from underlying asset to GHO (expressed in WAD), e.g. a ratio of 2e18 means 2 GHO per 1 underlying asset + uint256 public immutable PRICE_RATIO; + + /// @dev Underlying asset units represent units for the underlying asset + uint256 internal immutable _underlyingAssetUnits; + + /** + * @dev Constructor + * @param priceRatio The price ratio from underlying asset to GHO (expressed in WAD) + * @param underlyingAsset The address of the underlying asset + * @param underlyingAssetDecimals The number of decimals of the underlying asset + */ + constructor(uint256 priceRatio, address underlyingAsset, uint8 underlyingAssetDecimals) { + /// FunctionCallMutation of: require(priceRatio > 0, 'INVALID_PRICE_RATIO'); + 'INVALID_PRICE_RATIO'; + PRICE_RATIO = priceRatio; + UNDERLYING_ASSET = underlyingAsset; + UNDERLYING_ASSET_DECIMALS = underlyingAssetDecimals; + _underlyingAssetUnits = 10 ** underlyingAssetDecimals; + } + + /// @inheritdoc IGsmPriceStrategy + function getAssetPriceInGho(uint256 assetAmount, bool roundUp) external view returns (uint256) { + return + assetAmount.mulDiv( + PRICE_RATIO, + _underlyingAssetUnits, + roundUp ? Math.Rounding.Up : Math.Rounding.Down + ); + } + + /// @inheritdoc IGsmPriceStrategy + function getGhoPriceInAsset(uint256 ghoAmount, bool roundUp) external view returns (uint256) { + return + ghoAmount.mulDiv( + _underlyingAssetUnits, + PRICE_RATIO, + roundUp ? Math.Rounding.Up : Math.Rounding.Down + ); + } +} diff --git a/certora/GSM/mutations/mutants/priceStrategy/FixedPriceStrategy.sol7.sol b/certora/GSM/mutations/mutants/priceStrategy/FixedPriceStrategy.sol7.sol new file mode 100644 index 00000000..3c3a75a7 --- /dev/null +++ b/certora/GSM/mutations/mutants/priceStrategy/FixedPriceStrategy.sol7.sol @@ -0,0 +1,60 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.10; + +import {Math} from '@openzeppelin/contracts/utils/math/Math.sol'; +import {IGsmPriceStrategy} from './interfaces/IGsmPriceStrategy.sol'; + +/** + * @title FixedPriceStrategy + * @author Aave + * @notice Price strategy involving a fixed-rate conversion from an underlying asset to GHO + */ +contract FixedPriceStrategy is IGsmPriceStrategy { + using Math for uint256; + + /// @inheritdoc IGsmPriceStrategy + uint256 public constant GHO_DECIMALS = 18; + + /// @inheritdoc IGsmPriceStrategy + address public immutable UNDERLYING_ASSET; + + /// @inheritdoc IGsmPriceStrategy + uint256 public immutable UNDERLYING_ASSET_DECIMALS; + + /// @dev The price ratio from underlying asset to GHO (expressed in WAD), e.g. a ratio of 2e18 means 2 GHO per 1 underlying asset + uint256 public immutable PRICE_RATIO; + + /// @dev Underlying asset units represent units for the underlying asset + uint256 internal immutable _underlyingAssetUnits; + + /** + * @dev Constructor + * @param priceRatio The price ratio from underlying asset to GHO (expressed in WAD) + * @param underlyingAsset The address of the underlying asset + * @param underlyingAssetDecimals The number of decimals of the underlying asset + */ + constructor(uint256 priceRatio, address underlyingAsset, uint8 underlyingAssetDecimals) { + require(priceRatio > 0, 'INVALID_PRICE_RATIO'); + PRICE_RATIO = priceRatio; + UNDERLYING_ASSET = underlyingAsset; + UNDERLYING_ASSET_DECIMALS = underlyingAssetDecimals; + _underlyingAssetUnits = 10 ** underlyingAssetDecimals; + } + + /// @inheritdoc IGsmPriceStrategy + function getAssetPriceInGho(uint256 assetAmount, bool roundUp) external view returns (uint256) { + return + assetAmount.mulDiv( + PRICE_RATIO, + _underlyingAssetUnits, + roundUp ? Math.Rounding.Up : Math.Rounding.Down + ); + } + + /// @inheritdoc IGsmPriceStrategy + function getGhoPriceInAsset(uint256 ghoAmount, bool roundUp) external view returns (uint256) { + return + /// FunctionCallMutation of: ghoAmount.mulDiv( + _underlyingAssetUnits; + } +} diff --git a/certora/GSM/mutations/mutants/priceStrategy/FixedPriceStrategy.sol9 copy.sol b/certora/GSM/mutations/mutants/priceStrategy/FixedPriceStrategy.sol9 copy.sol new file mode 100644 index 00000000..01ecb2bd --- /dev/null +++ b/certora/GSM/mutations/mutants/priceStrategy/FixedPriceStrategy.sol9 copy.sol @@ -0,0 +1,64 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.10; + +import {Math} from '@openzeppelin/contracts/utils/math/Math.sol'; +import {IGsmPriceStrategy} from './interfaces/IGsmPriceStrategy.sol'; + +/** + * @title FixedPriceStrategy + * @author Aave + * @notice Price strategy involving a fixed-rate conversion from an underlying asset to GHO + */ +contract FixedPriceStrategy is IGsmPriceStrategy { + using Math for uint256; + + /// @inheritdoc IGsmPriceStrategy + uint256 public constant GHO_DECIMALS = 18; + + /// @inheritdoc IGsmPriceStrategy + address public immutable UNDERLYING_ASSET; + + /// @inheritdoc IGsmPriceStrategy + uint256 public immutable UNDERLYING_ASSET_DECIMALS; + + /// @dev The price ratio from underlying asset to GHO (expressed in WAD), e.g. a ratio of 2e18 means 2 GHO per 1 underlying asset + uint256 public immutable PRICE_RATIO; + + /// @dev Underlying asset units represent units for the underlying asset + uint256 internal immutable _underlyingAssetUnits; + + /** + * @dev Constructor + * @param priceRatio The price ratio from underlying asset to GHO (expressed in WAD) + * @param underlyingAsset The address of the underlying asset + * @param underlyingAssetDecimals The number of decimals of the underlying asset + */ + constructor(uint256 priceRatio, address underlyingAsset, uint8 underlyingAssetDecimals) { + /// RequireMutation of: require(priceRatio > 0, 'INVALID_PRICE_RATIO'); + require(!(priceRatio > 0), 'INVALID_PRICE_RATIO'); + PRICE_RATIO = priceRatio; + UNDERLYING_ASSET = underlyingAsset; + UNDERLYING_ASSET_DECIMALS = underlyingAssetDecimals; + _underlyingAssetUnits = 10 ** underlyingAssetDecimals; + } + + /// @inheritdoc IGsmPriceStrategy + function getAssetPriceInGho(uint256 assetAmount, bool roundUp) external view returns (uint256) { + return + assetAmount.mulDiv( + PRICE_RATIO, + _underlyingAssetUnits, + roundUp ? Math.Rounding.Up : Math.Rounding.Down + ); + } + + /// @inheritdoc IGsmPriceStrategy + function getGhoPriceInAsset(uint256 ghoAmount, bool roundUp) external view returns (uint256) { + return + ghoAmount.mulDiv( + _underlyingAssetUnits, + PRICE_RATIO, + roundUp ? Math.Rounding.Up : Math.Rounding.Down + ); + } +} diff --git a/certora/GSM/mutations/mutants/priceStrategy/FixedPriceStrategy.sol9.sol b/certora/GSM/mutations/mutants/priceStrategy/FixedPriceStrategy.sol9.sol new file mode 100644 index 00000000..73a72d61 --- /dev/null +++ b/certora/GSM/mutations/mutants/priceStrategy/FixedPriceStrategy.sol9.sol @@ -0,0 +1,64 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.10; + +import {Math} from '@openzeppelin/contracts/utils/math/Math.sol'; +import {IGsmPriceStrategy} from './interfaces/IGsmPriceStrategy.sol'; + +/** + * @title FixedPriceStrategy + * @author Aave + * @notice Price strategy involving a fixed-rate conversion from an underlying asset to GHO + */ +contract FixedPriceStrategy is IGsmPriceStrategy { + using Math for uint256; + + /// @inheritdoc IGsmPriceStrategy + uint256 public constant GHO_DECIMALS = 18; + + /// @inheritdoc IGsmPriceStrategy + address public immutable UNDERLYING_ASSET; + + /// @inheritdoc IGsmPriceStrategy + uint256 public immutable UNDERLYING_ASSET_DECIMALS; + + /// @dev The price ratio from underlying asset to GHO (expressed in WAD), e.g. a ratio of 2e18 means 2 GHO per 1 underlying asset + uint256 public immutable PRICE_RATIO; + + /// @dev Underlying asset units represent units for the underlying asset + uint256 internal immutable _underlyingAssetUnits; + + /** + * @dev Constructor + * @param priceRatio The price ratio from underlying asset to GHO (expressed in WAD) + * @param underlyingAsset The address of the underlying asset + * @param underlyingAssetDecimals The number of decimals of the underlying asset + */ + constructor(uint256 priceRatio, address underlyingAsset, uint8 underlyingAssetDecimals) { + require(priceRatio > 0, 'INVALID_PRICE_RATIO'); + PRICE_RATIO = priceRatio; + UNDERLYING_ASSET = underlyingAsset; + UNDERLYING_ASSET_DECIMALS = underlyingAssetDecimals; + /// BinaryOpMutation of: _underlyingAssetUnits = 10 ** underlyingAssetDecimals; + _underlyingAssetUnits = 10 % underlyingAssetDecimals; + } + + /// @inheritdoc IGsmPriceStrategy + function getAssetPriceInGho(uint256 assetAmount, bool roundUp) external view returns (uint256) { + return + assetAmount.mulDiv( + PRICE_RATIO, + _underlyingAssetUnits, + roundUp ? Math.Rounding.Up : Math.Rounding.Down + ); + } + + /// @inheritdoc IGsmPriceStrategy + function getGhoPriceInAsset(uint256 ghoAmount, bool roundUp) external view returns (uint256) { + return + ghoAmount.mulDiv( + _underlyingAssetUnits, + PRICE_RATIO, + roundUp ? Math.Rounding.Up : Math.Rounding.Down + ); + } +} diff --git a/certora/steward/conf/rules.conf b/certora/steward/conf/rules.conf new file mode 100644 index 00000000..9585a2a3 --- /dev/null +++ b/certora/steward/conf/rules.conf @@ -0,0 +1,32 @@ +{ + "files": [ + "certora/steward/harness/GhoStewardV2_Harness.sol", + "src/contracts/facilitators/aave/interestStrategy/FixedRateStrategyFactory.sol" + ], + "link": [ + "GhoStewardV2_Harness:FIXED_RATE_STRATEGY_FACTORY=FixedRateStrategyFactory", + ], + "packages": [ + "@aave/core-v3/=lib/aave-v3-core", + "@aave/periphery-v3/=lib/aave-v3-periphery", + "@aave/=lib/aave-token", + "@openzeppelin/=lib/openzeppelin-contracts", + "aave-stk-v1-5/=lib/aave-stk-v1-5", + "ds-test/=lib/forge-std/lib/ds-test/src", + "forge-std/=lib/forge-std/src", + "aave-address-book/=lib/aave-address-book/src", + "aave-helpers/=lib/aave-stk-v1-5/lib/aave-helpers", + "aave-v3-core/=lib/aave-address-book/lib/aave-v3-core", + "erc4626-tests/=lib/aave-stk-v1-5/lib/openzeppelin-contracts/lib/erc4626-tests", + "openzeppelin-contracts/=lib/aave-stk-v1-5/lib/openzeppelin-contracts", + "solidity-utils/=lib/solidity-utils/src" + ], + "optimistic_loop": true, + "process": "emv", + "prover_args": ["-depth 15","-mediumTimeout 1000"], + "smt_timeout": "2000", + "solc": "solc8.10", + "verify": "GhoStewardV2_Harness:certora/steward/specs/rules.spec", + "rule_sanity": "basic", + "msg": "STEWARD: all rules" +} \ No newline at end of file diff --git a/certora/steward/conf/sanity.conf b/certora/steward/conf/sanity.conf new file mode 100644 index 00000000..b69e3c96 --- /dev/null +++ b/certora/steward/conf/sanity.conf @@ -0,0 +1,33 @@ +{ + "files": [ + "certora/steward/harness/GhoStewardV2_Harness.sol", + "src/contracts/facilitators/aave/interestStrategy/FixedRateStrategyFactory.sol" + ], + "link": [ + "GhoStewardV2_Harness:FIXED_RATE_STRATEGY_FACTORY=FixedRateStrategyFactory", + ], + "packages": [ + "@aave/core-v3/=lib/aave-v3-core", + "@aave/periphery-v3/=lib/aave-v3-periphery", + "@aave/=lib/aave-token", + "@openzeppelin/=lib/openzeppelin-contracts", + "aave-stk-v1-5/=lib/aave-stk-v1-5", + "ds-test/=lib/forge-std/lib/ds-test/src", + "forge-std/=lib/forge-std/src", + "aave-address-book/=lib/aave-address-book/src", + "aave-helpers/=lib/aave-stk-v1-5/lib/aave-helpers", + "aave-v3-core/=lib/aave-address-book/lib/aave-v3-core", + "erc4626-tests/=lib/aave-stk-v1-5/lib/openzeppelin-contracts/lib/erc4626-tests", + "openzeppelin-contracts/=lib/aave-stk-v1-5/lib/openzeppelin-contracts", + "solidity-utils/=lib/solidity-utils/src" + ], + "optimistic_loop": true, + "prover_args": ["-depth 15","-mediumTimeout 1000","-cache none"], + "smt_timeout": "2000", + "solc": "solc8.10", + "verify": "GhoStewardV2_Harness:certora/steward/specs/rules.spec", + "rule": ["sanity"], + "disable_auto_cache_key_gen" :true, + "cache" :"none", + "msg": "STEWARD::sanity" +} \ No newline at end of file diff --git a/certora/steward/harness/GhoStewardV2_Harness.sol b/certora/steward/harness/GhoStewardV2_Harness.sol new file mode 100644 index 00000000..c0b324ab --- /dev/null +++ b/certora/steward/harness/GhoStewardV2_Harness.sol @@ -0,0 +1,22 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.10; + +import {GhoStewardV2} from "../../../src/contracts/misc/GhoStewardV2.sol"; + + +contract GhoStewardV2_Harness is GhoStewardV2 { + constructor( + address owner, + address addressesProvider, + address ghoToken, + address fixedRateStrategyFactory, + address riskCouncil + ) GhoStewardV2 (owner,addressesProvider,ghoToken,fixedRateStrategyFactory,riskCouncil) { + } + + function get_gsmFeeStrategiesByRates(uint256 buyFee, uint256 sellFee) external view returns(address) { + return _gsmFeeStrategiesByRates[buyFee][sellFee]; + } + +} + diff --git a/certora/steward/specs/rules.spec b/certora/steward/specs/rules.spec new file mode 100644 index 00000000..883eabb0 --- /dev/null +++ b/certora/steward/specs/rules.spec @@ -0,0 +1,347 @@ +using FixedRateStrategyFactory as FAC; + + +/*=========================================================================== + This is a specification file for the contract GhoStewardV2. + The rules were written base on the following: + https://github.com/aave/gho-core/pull/388 + + We check the following aspects: + - Limitations due to timelocks. + - For the relevant functions, only autorized sender can call them. + - When setting new paramethers they are in the correct range. + - The new paramethers are indeed set. + =============================================================================*/ + +methods { + function _.getPool() external => NONDET; + function _.getConfiguration(address) external => NONDET; + function _.getPoolConfigurator() external => NONDET; + + function _.getBorrowCap(DataTypes.ReserveConfigurationMap memory) internal => + get_BORROW_CAP_cvl() expect uint256 ; + function _.setBorrowCap(address token, uint256 newCap) external => + set_BORROW_CAP_cvl(token,newCap) expect void ALL; + + function _.getBaseVariableBorrowRate() external => + get_BORROW_RATE_cvl() expect uint256; + function _.setReserveInterestRateStrategyAddress(address,address strategy) external => + set_STRATEGY(strategy) expect void ALL; + + function _.getExposureCap() external => get_EXPOSURE_CAP_cvl() expect uint256 ; + function _.updateExposureCap(uint128 newCap) external => + set_EXPOSURE_CAP_cvl(newCap) expect void ALL; + + function _.getBuyFee(uint256) external => get_BUY_FEE_cvl() expect uint256; + function _.getSellFee(uint256) external => get_SELL_FEE_cvl() expect uint256; + function _.updateFeeStrategy(address strategy) external => + set_FEE_STRATEGY(strategy) expect void ALL; + + + function owner() external returns (address) envfree; + function getGhoTimelocks() external returns (IGhoStewardV2.GhoDebounce) envfree; + function getGsmTimelocks(address) external returns (IGhoStewardV2.GsmDebounce) envfree; + function GHO_BORROW_RATE_CHANGE_MAX() external returns uint256 envfree; + function GSM_FEE_RATE_CHANGE_MAX() external returns uint256 envfree; + function GHO_BORROW_RATE_MAX() external returns uint256 envfree; + function MINIMUM_DELAY() external returns uint256 envfree; + function RISK_COUNCIL() external returns address envfree; + function FAC.getStrategyByRate(uint256) external returns (address) envfree; + function get_gsmFeeStrategiesByRates(uint256,uint256) external returns(address) envfree; +} + + +ghost uint256 BORROW_CAP { + axiom 1==1; +} +function get_BORROW_CAP_cvl() returns uint256 { + return BORROW_CAP; +} +function set_BORROW_CAP_cvl(address token, uint256 newCap) { + BORROW_CAP = newCap; +} + +ghost uint256 BORROW_RATE { + axiom BORROW_RATE <= 10^27; +} +function get_BORROW_RATE_cvl() returns uint256 { + return BORROW_RATE; +} + +ghost address STRATEGY { + axiom 1==1; +} +function set_STRATEGY(address strategy) { + STRATEGY = strategy; +} + + + +ghost uint128 EXPOSURE_CAP { + axiom 1==1; +} +function get_EXPOSURE_CAP_cvl() returns uint128 { + return EXPOSURE_CAP; +} +function set_EXPOSURE_CAP_cvl(uint128 newCap) { + EXPOSURE_CAP = newCap; +} + + +ghost uint128 BUY_FEE { + axiom 1==1; +} +function get_BUY_FEE_cvl() returns uint128 { + return BUY_FEE; +} +ghost uint128 SELL_FEE { + axiom 1==1; +} +function get_SELL_FEE_cvl() returns uint128 { + return SELL_FEE; +} +ghost address FEE_STRATEGY { + axiom 1==1; +} +function set_FEE_STRATEGY(address strategy) { + FEE_STRATEGY = strategy; +} + + + +/* ================================================================================= + ================================================================================ + Part 1: validity of the timelocks + ================================================================================= + ==============================================================================*/ + +// FUNCTION: updateGhoBorrowCap +rule ghoBorrowCapLastUpdate__updated_only_by_updateGhoBorrowCap(method f) { + env e; calldataarg args; + + uint40 ghoBorrowCapLastUpdate_before = getGhoTimelocks().ghoBorrowCapLastUpdate; + f(e,args); + uint40 ghoBorrowCapLastUpdate_after = getGhoTimelocks().ghoBorrowCapLastUpdate; + + assert (ghoBorrowCapLastUpdate_after != ghoBorrowCapLastUpdate_before) => + f.selector == sig:updateGhoBorrowCap(uint256).selector; +} + +rule updateGhoBorrowCap_update_correctly__ghoBorrowCapLastUpdate() { + env e; uint256 newBorrowCap; + updateGhoBorrowCap(e,newBorrowCap); + assert getGhoTimelocks().ghoBorrowCapLastUpdate == require_uint40(e.block.timestamp); +} + +rule updateGhoBorrowCap_timelock() { + uint40 ghoBorrowCapLastUpdate_before = getGhoTimelocks().ghoBorrowCapLastUpdate; + env e; uint256 newBorrowCap; + updateGhoBorrowCap(e,newBorrowCap); + + assert to_mathint(e.block.timestamp) > ghoBorrowCapLastUpdate_before + MINIMUM_DELAY(); +} + + +// FUNCTION: updateGhoBorrowRate +rule ghoBorrowRateLastUpdate__updated_only_by_updateGhoBorrowRate(method f) { + env e; calldataarg args; + + uint40 ghoBorrowRateLastUpdate_before = getGhoTimelocks().ghoBorrowRateLastUpdate; + f(e,args); + uint40 ghoBorrowRateLastUpdate_after = getGhoTimelocks().ghoBorrowRateLastUpdate; + + assert (ghoBorrowRateLastUpdate_after != ghoBorrowRateLastUpdate_before) => + f.selector == sig:updateGhoBorrowRate(uint256).selector; +} + +rule updateGhoBorrowRate_update_correctly__ghoBorrowRateLastUpdate() { + env e; uint256 newBorrowRate; + updateGhoBorrowRate(e,newBorrowRate); + assert getGhoTimelocks().ghoBorrowRateLastUpdate == require_uint40(e.block.timestamp); +} + +rule updateGhoBorrowRate_timelock() { + uint40 ghoBorrowRateLastUpdate_before = getGhoTimelocks().ghoBorrowRateLastUpdate; + env e; uint256 newBorrowRate; + updateGhoBorrowRate(e,newBorrowRate); + + assert to_mathint(e.block.timestamp) > ghoBorrowRateLastUpdate_before + MINIMUM_DELAY(); +} + + + +// FUNCTION: updateGsmExposureCap +rule gsmExposureCapLastUpdated__updated_only_by_updateGsmExposureCap(method f) { + env e; calldataarg args; + address gsm; + + uint40 gsmExposureCapLastUpdated_before = getGsmTimelocks(gsm).gsmExposureCapLastUpdated; + f(e,args); + uint40 gsmExposureCapLastUpdated_after = getGsmTimelocks(gsm).gsmExposureCapLastUpdated; + + assert (gsmExposureCapLastUpdated_after != gsmExposureCapLastUpdated_before) => + f.selector == sig:updateGsmExposureCap(address,uint128).selector; +} + +rule updateGsmExposureCap_update_correctly__gsmExposureCapLastUpdated() { + env e; address gsm; uint128 newExposureCap; + updateGsmExposureCap(e,gsm, newExposureCap); + assert getGsmTimelocks(gsm).gsmExposureCapLastUpdated == require_uint40(e.block.timestamp); +} + +rule updateGsmExposureCap_timelock() { + env e; address gsm; uint128 newExposureCap; + uint40 gsmExposureCapLastUpdated_before = getGsmTimelocks(gsm).gsmExposureCapLastUpdated; + updateGsmExposureCap(e,gsm, newExposureCap); + + assert to_mathint(e.block.timestamp) > gsmExposureCapLastUpdated_before + MINIMUM_DELAY(); +} + + + +// FUNCTION: updateGsmBuySellFees +rule gsmFeeStrategyLastUpdated__updated_only_by_updateGsmBuySellFees(method f) { + env e; calldataarg args; + address gsm; + + uint40 gsmFeeStrategyLastUpdated_before = getGsmTimelocks(gsm).gsmFeeStrategyLastUpdated; + f(e,args); + uint40 gsmFeeStrategyLastUpdated_after = getGsmTimelocks(gsm).gsmFeeStrategyLastUpdated; + + assert (gsmFeeStrategyLastUpdated_after != gsmFeeStrategyLastUpdated_before) => + f.selector == sig:updateGsmBuySellFees(address,uint256,uint256).selector; +} + +rule updateGsmBuySellFees_update_correctly__gsmFeeStrategyLastUpdated() { + env e; address gsm; uint256 buyFee; uint256 sellFee; + updateGsmBuySellFees(e,gsm, buyFee, sellFee); + assert getGsmTimelocks(gsm).gsmFeeStrategyLastUpdated == require_uint40(e.block.timestamp); +} + +rule updateGsmBuySellFees_timelock() { + env e; address gsm; uint256 buyFee; uint256 sellFee; + uint40 gsmFeeStrategyLastUpdated_before = getGsmTimelocks(gsm).gsmFeeStrategyLastUpdated; + updateGsmBuySellFees(e,gsm, buyFee, sellFee); + + assert to_mathint(e.block.timestamp) > gsmFeeStrategyLastUpdated_before + MINIMUM_DELAY(); +} + + + + +/* ================================================================================= + ================================================================================ + Part 2: autorized message sender + ================================================================================= + ==============================================================================*/ +rule only_RISK_COUNCIL_can_call__updateFacilitatorBucketCapacity() { + env e; address facilitator; uint128 newBucketCapacity; + + updateFacilitatorBucketCapacity(e,facilitator,newBucketCapacity); + assert (e.msg.sender==RISK_COUNCIL()); +} +rule only_RISK_COUNCIL_can_call__updateGhoBorrowCap() { + env e; uint256 newBorrowCap; + + updateGhoBorrowCap(e,newBorrowCap); + assert (e.msg.sender==RISK_COUNCIL()); +} +rule only_RISK_COUNCIL_can_call__updateGhoBorrowRate() { + env e; uint256 newBorrowRate; + + updateGhoBorrowRate(e,newBorrowRate); + assert (e.msg.sender==RISK_COUNCIL()); +} +rule only_RISK_COUNCIL_can_call__updateGsmExposureCap() { + env e; address gsm; uint128 newExposureCap; + + updateGsmExposureCap(e,gsm,newExposureCap); + assert (e.msg.sender==RISK_COUNCIL()); +} +rule only_RISK_COUNCIL_can_call__updateGsmBuySellFees() { + env e; address gsm; uint256 buyFee; uint256 sellFee; + + + updateGsmBuySellFees(e,gsm,buyFee,sellFee); + assert (e.msg.sender==RISK_COUNCIL()); +} +rule only_owner_can_call__setControlledFacilitator() { + env e; + address[] facilitatorList; + bool approve; + + setControlledFacilitator(e,facilitatorList,approve); + assert (e.msg.sender==owner()); +} + + + +/* ================================================================================= + ================================================================================ + Part 3: correctness of the main functions. + We check the validity of the new paramethers values, and that are indeed set. + ================================================================================= + ==============================================================================*/ +rule updateGhoBorrowCap__correctness() { + env e; uint256 newBorrowCap; + uint256 borrow_cap_before = BORROW_CAP; + updateGhoBorrowCap(e,newBorrowCap); + assert BORROW_CAP==newBorrowCap; + + uint256 borrow_cap_after = BORROW_CAP; + assert borrow_cap_before <= borrow_cap_after && to_mathint(borrow_cap_after) <= 2*borrow_cap_before; +} + + +rule updateGhoBorrowRate__correctness() { + env e; uint256 newBorrowRate; + uint256 borrow_rate_begore = BORROW_RATE; + updateGhoBorrowRate(e,newBorrowRate); + assert FAC.getStrategyByRate(newBorrowRate) == STRATEGY; + + assert (borrow_rate_begore-GHO_BORROW_RATE_CHANGE_MAX() <= to_mathint(newBorrowRate) + && + to_mathint(newBorrowRate) <= borrow_rate_begore+GHO_BORROW_RATE_CHANGE_MAX()); + assert (newBorrowRate <= GHO_BORROW_RATE_MAX()); +} + + +rule updateGsmExposureCap__correctness() { + env e; address gsm; uint128 newExposureCap; + uint128 exposure_cap_before = EXPOSURE_CAP; + updateGsmExposureCap(e,gsm,newExposureCap); + assert EXPOSURE_CAP==newExposureCap; + + uint128 exposure_cap_after = EXPOSURE_CAP; + assert exposure_cap_before <= exposure_cap_after && + to_mathint(exposure_cap_after) <= 2*exposure_cap_before; +} + + +rule updateGsmBuySellFees__correctness() { + env e; address gsm; uint256 buyFee; uint256 sellFee; + uint256 buyFee_before = BUY_FEE; + uint256 sellFee_before = SELL_FEE; + updateGsmBuySellFees(e,gsm,buyFee,sellFee); + assert get_gsmFeeStrategiesByRates(buyFee,sellFee)==FEE_STRATEGY; + + assert to_mathint(buyFee) <= buyFee_before + GSM_FEE_RATE_CHANGE_MAX(); + assert to_mathint(sellFee) <= sellFee_before + GSM_FEE_RATE_CHANGE_MAX(); +} + + + + + + + +/* ================================================================================= + Rule: sanity. + Status: PASS. + ================================================================================*/ +rule sanity(method f) { + env e; + calldataarg args; + f(e,args); + satisfy true; +}