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.

Exchange Rate Consistency​

The Exchange Rate Consistency invariant ensures that the vault’s exchange rate is consistent with ERC-4626 floor rounding. The invariant is defined via a round-trip: convert all shares to assets, then convert those assets back to shares. Because of two successive floor divisions, the round-trip can lose at most a bounded number of shares.

Definitions​

  • S = totalSupply
  • A = totalAssets
  • vS = S + 10^offset
  • vA = A + 1

ERC-4626 conversion rules implemented by the vault:

  • convertToAssets(shares) = floor(shares × vA / vS)
  • convertToShares(assets) = floor(assets × vS / vA)

The round-trip using the full supply is:

  • assets = floor(S × vA / vS)
  • shares = floor(assets × vS / vA)

where shares here denotes the result of convertToShares(convertToAssets(S)).

Invariant​

∀ v ∈ V : vault.totalSupply() > 0 ⟹
    Let S = vault.totalSupply()
    Let A = vault.totalAssets()
    Let offset = vault._decimalsOffset()
    Let vS = S + 10 ^ offset
    Let vA = A + 1
    Let D_max = ceil((vS − 1) / vA)

    Let assets = floor(S × vA / vS)
    Let shares = floor(assets × vS / vA)

    // Round-trip deficit within ERC-4626 arithmetic bound
    0 ≤ S − shares ≤ D_max

Prices Consistency​

The Prices Consistency invariant ensures that when the system is in an Idle state, 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 ^ config.priceAdapterDecimals()
Let underlyingDecimals = config.getTokenDecimals(underlyingAsset)

LO.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 = LO.getAssetPrices(token)
            Let tokenDecimals = config.getTokenDecimals(token)
            Let rawValue = price × shares / priceAdapterPrecision
            Let value = convertDecimals(rawValue, tokenDecimals, underlyingDecimals)
            totalAssets += value
        vault.totalAssets() = totalAssets

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, StateCommitment​

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

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

Liquidity Orchestrator Phase: SellingLeg or BuyingLeg​

Order generation runs offchain in the zkVM. The following balance relationships are therefore verified at zkVM payload generation: the keeper reads onchain state (LO balances, current phase), runs the zkVM to produce the order payload, then checks these invariants against the generated orders and onchain balances. If any check fails, the payload is rejected and no proof is submitted.

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

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