Skip to main content

Protocol Invariants

This page documents the protocol invariants that are continuously monitored in production to ensure the security and correctness of the Orion Finance Protocol.

Protocol invariants are properties that must always hold true for the protocol to function correctly. These are continuously monitored in production to detect any violations that could indicate bugs, exploits, or unexpected behavior.

Invariant 1: Token Balance Conservation​

The Token Balance Conservation invariant ensures that the accounting of tokens is correct. Specifically, for every token managed by the system (both underlying and non-underlying assets), the sum of balances tracked in all vaults and orchestrators always reflects exactly the real token balances held by the Liquidity Orchestrator contract.

This invariant is strictly formalized in different protocol phases.

Liquidity Orchestrator Phase: Idle or SellingLeg​

∀ t ∈ T : t ≠ U ⟹
    (Σ(v ∈ V) vault.getPortfolio()[t]) = IERC20(t).balanceOf(address(LO))

∀ t ∈ T : t = U ⟹
    (Σ(v ∈ V) vault.getPortfolio()[U])
    + ISO.bufferAmount()
    + ISO.pendingProtocolFees()
    + (Σ(v ∈ V) vault.pendingVaultFees())
    + (Σ(v ∈ V) vault.pendingDeposit(maxFulfillBatchSize))
    = IERC20(U).balanceOf(address(LO))

Liquidity Orchestrator Phase: BuyingLeg​

∀ t ∈ T : t ≠ U ⟹
    (Σ(v ∈ V) vault.getPortfolio()[t])
    = IERC20(t).balanceOf(address(LO)) + ISO.getOrders(true)[t]

∀ t ∈ T : t = U ⟹
    (Σ(v ∈ V) vault.getPortfolio()[U])
    + ISO.bufferAmount()
    + ISO.pendingProtocolFees()
    + (Σ(v ∈ V) vault.pendingVaultFees())
    + (Σ(v ∈ V) vault.pendingDeposit(maxFulfillBatchSize))
    + LO.deltaBufferAmount()
    = IERC20(U).balanceOf(address(LO)) + ISO.getOrders(true)[U]

Invariant 2: Buffer Amount​

The Buffer Amount invariant ensures that the protocol always maintains a sufficient buffer of the underlying asset to facilitate operations efficiently. This buffer acts as a liquidity reserve calculated as a fraction of the total assets managed by all vaults.

Let V = {v : v is a transparent vault in the current epoch}
Let protocolTotalAssets = Σ(v ∈ V) ISO.getVaultTotalAssetsAll(v)[2]
Let targetBufferAmount = protocolTotalAssets × LO.targetBufferRatio() / BASIS_POINTS_FACTOR

ISO.currentPhase() ∈ {PostprocessingTransparentVaults, BuildingOrders} ⟹
    ISO.bufferAmount() ≥ targetBufferAmount

Invariant 3: Prices Consistency​

The Prices Consistency invariant ensures that when the system is in an Idle state (both the Liquidity Orchestrator and Internal State Orchestrator are idle), the total assets reported by each vault must exactly match the calculated value of its portfolio when priced using the protocol's price feeds. This invariant guarantees that the vault's internal accounting (totalAssets()) remains synchronized with the actual market value of its holdings as determined by the price oracles.

Let V = {v : v is a transparent vault}
Let priceAdapterPrecision = 10 ^ ISO.priceAdapterDecimals()
Let underlyingDecimals = config.getTokenDecimals(underlyingAsset)

LO.currentPhase() == Idle ∧ ISO.currentPhase() == Idle ⟹
    ∀ v ∈ V :
        Let (tokens, sharesPerAsset) = vault.getPortfolio()
        Let n = length(tokens)
        Let totalAssets = 0
        For i = 0 to n-1:
            Let token = tokens[i]
            Let shares = sharesPerAsset[i]
            Let price = ISO.getPriceOf(token)
            Let tokenDecimals = config.getTokenDecimals(token)
            Let rawValue = price × shares / priceAdapterPrecision
            Let value = convertDecimals(rawValue, tokenDecimals, underlyingDecimals)
            totalAssets += value
        vault.totalAssets() = totalAssets

Invariant 4: Self-Financing Condition​

Invariant: When the LO phase is either SellingLeg or BuyingLeg, the protocol's rebalancing operations must be self-financing: the value of sell orders (ISO.getOrders(true)) plus the underlying assets paid out for redemptions must equal the value of buy orders (ISO.getOrders(false)) plus the underlying assets to be received from deposits, after adjusting for pending deposits and pending redeems. This balance ensures no external capital injection is needed and prevents accumulation of excess capital during rebalancing.

LO.currentPhase() ∈ {SellingLeg, BuyingLeg} ⟹
    Let pendingRedeemAssets(v)
    = vault.convertToAssetsWithPITTotalAssets(
        vault.pendingRedeem(maxFulfillBatchSize),
        ISO.getVaultTotalAssetsAll(v)[0], Rounding.Floor)

    dotProduct(ISO.getOrders(true), ISO.getPriceOf())
    + Σ(v ∈ V) pendingRedeemAssets(v)
    = dotProduct(ISO.getOrders(false), ISO.getPriceOf())
    + Σ(v ∈ V) vault.pendingDeposit(maxFulfillBatchSize)

Invariant 5: Price Positivity​

The Price Positivity invariant ensures that all prices must be positive when queried, when ISO phase is not PreprocessingTransparentVaults.

ISO.currentPhase() ≠ PreprocessingTransparentVaults ⟹
    ∀ token ∈ T : ISO.getPriceOf(token) > 0

Invariant 6: Exchange Rate Consistency​

The Exchange Rate Consistency invariant ensures that the exchange rate must be consistent: converting all shares to assets and back to shares should preserve the total supply, regardless of phase.

∀ v ∈ V : vault.totalSupply() > 0 ⟹
    Let shares = vault.totalSupply()
    Let assets = vault.totalAssets()
    Let decimalsOffset = vault._decimalsOffset()
    Let virtualSupply = shares + 10 ^ decimalsOffset
    Let virtualAssets = assets + 1

    // Step 1: Convert all shares to assets (Floor)
    Let assetsFromShares = (shares × virtualAssets) / virtualSupply

    // Step 2: Convert those assets back to shares (Floor)
    Let sharesFromAssets = (assetsFromShares × virtualSupply) / virtualAssets

    // The round-trip should preserve totalSupply
    sharesFromAssets = shares
Last updated on