Protocol Invariants

Protocol Invariants

These properties describe the protocol's accounting, authorization, and risk boundaries. Each property has a scope: a reserve check, a health check, and a proof of full market backing are different guarantees.

This reference summarizes the runtime invariant register. The register identifies enforcement surfaces and verification limits. Tests and formal rules provide evidence under their own assumptions; their presence does not establish a completed proof or correct deployment wiring.

Accounting and indexes

Property	Boundary and limitation
Revenue is part of total supply	0 <= revenue_shares <= supplied_shares. Revenue minting and claims change both totals equally; seized collateral is reclassified without creating supply. This relationship alone does not prove backing.
Tracked cash limits payouts	Borrowing, withdrawals, flash loans, and revenue payouts respect tracked market reserves. Direct token donations do not increase tracked cash.
Token-funded credit uses measured receipts	Supply, repayment, and recapitalization account for what the pool receives. Requested amounts alone do not establish credit.
Positive position changes require shares	Positive supply/borrow must mint shares; positive net repayment/withdrawal must burn shares. Same-asset net settlement must burn both sides. Zero-share results at these boundaries revert.
Borrow index is monotone and bounded	Successful accrual cannot lower it and caps it at 10^36 raw RAY. It stops accruing interest at the ceiling; representability can still fail before that ceiling.
Supply index is bounded	It stays within 10^24 to 10^36 raw RAY. Ordinary interest distribution cannot lower it; debt writeoff can. The floor can preserve an unbacked residual claim.
Interest has an explicit split	At the RAY-value split, accrued interest equals supplier rewards plus the reserve-factor fee. Index and revenue-share rounding can leave value unrepresented; exact booked-value conservation is not guaranteed.

Borrow draws also reserve a cash buffer of 200 BPS of floored supplied token value. Borrowing, ordinary withdrawal, and revenue claims enforce their market utilization gate; liquidation withdrawal skips that gate. Selected exits reject zero total supply with outstanding debt. Accrual, liquidation, and writeoff do not maintain a universal utilization or full-backing guarantee.

For scales, rounding, accrual cadence, and accounting formulas, read Accounting and Numeric Domains. Reserve and recapitalization behavior belongs in Central Pool.

Account risk and liquidation

Debt-bearing borrowing, ordinary withdrawal, and account strategies require final LTV coverage, health factor at least 1, and the enabled minimum collateral floor. Listed LTV refreshes before the shared gate. Risk valuation floors collateral and weights, ceils debt, and floors health factor with saturation. See Health Factor and Collateral.

Ordinary liquidation requires debt and health below 1. Repayment and collateral seizure stay coupled through measured receipts and per-position seizure caps. Credit mode conserves seized shares as receiver credit plus protocol fee. Neither liquidation nor cleanup asserts final account health or full market backing. See Risk and Liquidations.

Configuration limits

Risk parameters use BPS, where 10,000 is 100%; indexes and rates use RAY (10^27), and health uses WAD (10^18).

Configuration	Required bound
Listing LTV and threshold	0 <= LTV < threshold <= 10,000
Threshold and bonus	threshold × (10,000 + bonus) <= 10,000²
Protocol fee on liquidation bonus	0 <= fee < 10,000
Liquidation target health	1 < target <= 10
Maximum-bonus health	0 < max_bonus_health < target
Bonus increment factor	0 < factor <= 10,000 BPS
Minimum LTV-weighted collateral	Nonnegative; 0 disables the floor
Supply and borrow caps	Nonnegative and representable in the asset-to-RAY conversion; 0 admits no positive entry
Supply and borrow position limits	Each configured limit is between 1 and 5; existing positions remain usable after a reduction
Account delegates	At most 16 grants
Reserve factor	Below 10,000 BPS
Flash-loan fee	At most 500 BPS
Utilization breakpoints	0 < mid < optimal < RAY, and optimal <= maximum <= RAY
Borrow-rate curve	Nonnegative base; nondecreasing slope parameters from base through maximum; maximum exceeds base and does not exceed MAX_BORROW_RATE_RAY

The threshold/bonus product is a configuration constraint, not a guarantee that all debt remains collectible after a price move. Execution separately caps seizure at actual collateral. Spoke listing edits validate bounds at execution, and an asset can be delisted only when its supplied and borrowed usage are both zero.

Token decimals are read during admission. Oracle source, timestamp, tolerance, sanity-band, and composite-asset constraints are maintained in Oracle System. Required valuations fail closed; configured dual sources require both legs, while explicitly admitted single-source configurations have their own checks.

Authority and emergency controls

The deployment path wires governance to own the controller and the controller to own the central pool. Pool accounting mutations authenticate their owner; correct ownership wiring remains a deployment obligation.

Account spending follows the current position-NFT owner or that owner's active registered delegate. The account's spoke binding is immutable. Delegates can choose payout recipients and have substantial economic authority; Managing Positions describes grants and NFT transfers.

Global pause, listing pause, listing freeze, and no_seize have different effects. Emergency restrictions only tighten through the immediate flag path; reopening is timelocked under the governance wiring. Permissionless cleanup bypasses pause and listing flags but retains insolvency, pricing, and flash-guard checks. See Governance and Timelock.

External calls and storage

Cash flash loans enforce exact balance settlement. For initial balance B, principal P, and fee F, the pool requires B − P after payout and after the callback, pulls P + F through receiver allowance, then requires B + F. Direct callback repayment does not satisfy this sequence.

Strategy authorization binds one exact input transfer. The controller measures router spending and output rather than trusting its return value, then checks final account risk. Router minimum-output validation and recipient receipt are separate guarantees. See Flash Loans and Strategies.

Account metadata, supply positions, debt positions, delegates, and NFT ownership have distinct storage lifetimes. Positions use hub-asset keys. Account creation and removal pair with NFT minting and burning, but TTL renewal is not identical across those records. Archived ownership must be restored before ownership-dependent flows can execute; account_exists checks metadata only.

Verification references

• Runtime invariant register
• Shared validation
• Rate-model validation
• Formal Verification
• Testing and Quality