# Overview

This document lists possible invariants to test, verify, or take into consideration when developing the GSM.

# Invariant List

### Price and Fee Strategies Invariants

1. In the price strategy, the inverse action of `getAssetPriceInGho` is `getGhoPriceInAsset`, which means that `assetAmount == getGhoPriceInAsset(getAssetPriceInGho(assetAmount))` holds always true
2. The view function `getGhoAmountForBuyAsset` is the inverse of `getAssetAmountForBuyAsset`. Similarly, `getGhoAmountForSellAsset` is the inverse of `getAssetAmountForSellAsset`. So it is possible to go from `assetAmount` to `ghoTotalAmount` and the other way around in a consistent way. (e.g. `assetAmount = getAssetAmountForBuyAsset(getGhoAmountForBuyAsset(assetAmount))` )

### Buy/Sell Invariants

1. Buying/selling should never be possible when the GSM is frozen and/or after it has been seized.
2. It should never be possible for `_currentExposure` of a GSM to exceed the `_exposureCap` as a result of a call to `sellAsset`.
3. If the `_currentExposure` exceeds the `_exposureCap`, `sellAsset` should revert until the `_currentExposure` is reduced below the `_exposureCap`.
4. When calling `buyAsset` successfully (i.e., no revert), the `_currentExposure` should always decrease.
5. When calling `sellAsset` successfully (i.e., no revert), the `_currentExposure` should always increase.
6. In case of using a 1:1 ratio and 0 fees, the inverse action of `buyAsset` must be `sellAsset`. (e.g. if `buyAsset(x assets)` needs `y GHO`, `sellAsset(x assets)` gives `y GHO`).

### Fees, Yield, and Backing

1. `_accruedFees` should never decrease, unless fees are being harvested by Treasury
2. In the event the underlying asset increases in value relative to the amount of GHO minted, excess yield harvesting should never result in previously-minted GHO having less backing (i.e., as new GHO is minted backed by the excess, it should not result in the GSM becoming under-backed in the same block).
3. In the event the underlying asset decreases in value relative to the amount of GHO minted, sending GHO or the underlying asset via `backWith` should not result in a state where the asset could immediately have yield to harvest.
4. “Gifting” GHO or the underlying asset to the GSM should never impact internal accounting of fees, yield, backing, etc.

### Token Rescue

1. Rescuing GHO should never result in there being less GHO available (as an ERC-20 balance) in the GSM than `_accruedFees`.
2. Rescuing the underlying asset should never result in there being less of the underlying (as an ERC-20 balance) than the combined total of the `_currentExposure` and `_tokenizedAssets`.

### Tokenized Assets

1. Seizure of the GSM should never include already-tokenized assets.
2. Once an underlying asset represents a tokenized obligation, it cannot move out of the GSM except during a call to `redeemTokenizedAsset`.
3. The `totalSupply` of the `GsmToken` should always be equal to the `_tokenizedAssets` GSM variable (in a simple case, where the GSM is the only minter/burner of the `GsmToken`).