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. Each invariant is implemented as either an offchain watchdog script or a zkVM-internal assertion. A violation triggers an automatic response, either pausing the Liquidity Orchestrator or rejecting the order payload.
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.
Summary
| Invariant | Scope | Phase Condition | Enforcement Point | On Violation |
|---|---|---|---|---|
| Exchange Rate Consistency | All transparent vaults | Always | Watchdog script | Pause LO |
| Liquidity Orchestrator Balance Consistency | All whitelisted assets | Idle, StateCommitment, SellingLeg, BuyingLeg | Watchdog script | Pause LO |
| Prices Consistency | All transparent vaults | Idle only | Watchdog script | Pause LO |
| Self-Financing Condition | Full epoch | SellingLeg, BuyingLeg | zkVM payload generation | Payload rejected |
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=vault.totalSupply()A=vault.totalAssets()offset: decimals offset used by the vaultvS=S + 10^offset(virtual supply)vA=A + 1(virtual assets)
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 ⟹
assets = floor(S × vA / vS)
shares = floor(assets × vS / vA)
D_max = ceil((vS − 1) / vA)
0 ≤ S − shares ≤ D_max
Violation interpretations:
S − shares > D_max: impossible under correct ERC-4626 arithmetic; indicates corrupted vault state or incorrecttotalAssetsaccounting.shares > S: impossible under floor rounding; indicates inflatedtotalAssets.
Enforcement
The watchdog runs against all vaults registered in OrionConfig. On any violation it calls LiquidityOrchestrator.pause().
Liquidity Orchestrator Balance Consistency
Verifies that every token's actual ERC-20 balance held by the Liquidity Orchestrator equals the sum of all tracked balances (vault portfolios, decommissioned vault portfolios, buffer, fees, pending deposits), adjusted for in-flight trades in trading phases. The check is phase-specific.
Phase: Idle or StateCommitment
All assets are checked with strict equality.
Non-underlying assets (t ≠ U):
∀ t ∈ T \ {U} :
Σ(v ∈ V) vault.getPortfolio()[t]
= IERC20(t).balanceOf(address(LO))
Underlying asset (t = U):
Σ(v ∈ V) vault.getPortfolio()[U]
+ Σ(v ∈ D) vault.getPortfolio()[U]
+ LO.bufferAmount()
+ LO.pendingProtocolFees()
+ Σ(v ∈ V) vault.pendingVaultFees()
+ Σ(v ∈ V) vault.pendingDeposit(maxFulfillBatchSize)
= IERC20(U).balanceOf(address(LO))
where D is the set of decommissioned vaults returned by config.getAllDecommissionedVaults(). Decommissioned vaults retain their underlying portfolio in the LO until fully settled.
Phase: SellingLeg or BuyingLeg
Non-underlying balances are allowed to deviate from portfolio entries by the value of executed trades at epoch prices. The underlying balance is checked strictly after accounting for those trade values.
-
delta_balance= value in underlying units of non-underlying balance mismatches at epoch prices (direction:portfolio − actualfor SellingLeg,actual − portfoliofor BuyingLeg). -
buffer_variationcaptures how the buffer has progressed within the current epoch relative to the buffer checkpoint used by the balance accounting logic. The resulting variation is then applied on top of the epoch-start buffer baseline so that the watchdog can compareIERC20(U).balanceOf(LO)with the portfolio and all pending components.
Expected underlying balance:
expected_underlying
= Σ(v ∈ V) portfolio[U]
+ Σ(v ∈ D) portfolio[U]
+ buffer_first
+ pendingProtocolFees
+ Σ(v ∈ V) pendingVaultFees
+ Σ(v ∈ V) pendingDeposit
+ buffer_variation
± delta_balance
IERC20(U).balanceOf(LO) = expected_underlying
Enforcement
On any violation in Idle, StateCommitment, SellingLeg, or BuyingLeg the watchdog calls LiquidityOrchestrator.pause().
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 prices = LO.getAssetPrices(tokens)
Let precision = 10 ^ config.priceAdapterDecimals()
Let uDecimals = config.getTokenDecimals(underlyingAsset)
D = Σ_i convertDecimals(
floor(prices[i] × sharesPerAsset[i] / precision),
tokenDecimals[i],
uDecimals
)
vault.totalAssets() = D
Enforcement
On any violation the watchdog calls LiquidityOrchestrator.pause().
Self-Financing Condition
When the LO phase is either SellingLeg or BuyingLeg, the protocol's rebalancing operations must be self-financing: the value of sell orders plus the underlying assets paid out for redemptions must equal (up to dust tolerance) the value of buy orders 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.
Because order generation runs offchain in the zkVM, this invariant is verified at zkVM payload generation: the keeper computes the generated orders (sell leg, buy leg, buffer delta, vault state updates) and runs the self-financing check before producing the proof fixture. If the check fails, the payload is rejected.
buffer_input + D + Σ_v Δ(totalAssets_v)⁻
= buffer_computed + R + ΔF_protocol + ΔF_vaults + Σ_v Δ(totalAssets_v)⁺
Equivalently:
D − R = ΔL + ΔF + Σ_v Δ(totalAssets_v)
where:
| Symbol | Definition |
|---|---|
D | Σ_v vault.pendingDeposit() — underlying flowing in from user deposits |
R | states.redemption_outflow — underlying flowing out to redeeming users |
ΔL | buffer_computed − buffer_input — change in LO free underlying reserve |
ΔF | epoch_protocol_fees + Σ_v (management_fee_v + performance_fee_v) — fees accrued this epoch |
Δ(totalAssets_v) | final_total_assets_v − input_total_assets_v per vault, split into positive (⁺) and negative (⁻) parts |
buffer_input | epoch_buffer_history[0] — buffer at epoch start (before any trades) |
buffer_computed | states.buffer_amount — buffer in the generated payload |
Enforcement
assert_self_financing() is called during zkVM payload generation, preventing an invalid proof fixture from being produced. The keeper will not submit a transaction for that epoch until a valid payload is generated.