Invariants

This page documents the invariant properties verified by the protocol’s test suites. Invariant tests use handler-based fuzzing to exercise random sequences of protocol operations, then verify that core safety properties hold after every action.

Running Invariant Tests

Invariant tests are excluded from default forge test runs due to their computational cost. To run all tests including invariants:

FOUNDRY_PROFILE=full forge test

The configuration uses runs = 256 and depth = 64 for the invariant fuzzer, with fail_on_revert = false to allow natural reverts during fuzzing.

PositionManager Invariants

The PositionManager test suite verifies 11 invariants across 21 handler actions, covering the core vault accounting, fee bounds, and liquidation mechanics.

ID	Invariant	Verification
PM-1	totalAssets = collateralQuoted - debt	Direct assertion on the accounting identity
PM-2	No zero-share minting (virtual offset inflation-attack protection)	Checks share conversion with virtual offset formula
PM-3	Burn preserves aggregate LTV	Ghost variable captures LTV before/after each burn (with forced interest accrual); cross-multiplication check includes rounding tolerance for fee-accrual-induced division errors
PM-4	Fee parameters within bounds	Checks base (managementFee)/performance fees ≤ 5000 bps
PM-5	Rebalance loss bounded by maxRebalanceLoss	Ghost variable captures totalAssets before/after rebalance
PM-6	Queue entries are registered borrow modules	Iterates supply/withdrawal queues and asserts isBorrowModule()
PM-7	Debt-free borrow positions are always healthy	Asserts isHealthy(safeLtv) when totalBorrowed == 0
PM-8	Pre-liquidation gating — reverts on healthy positions	Uses try/catch to verify revert when isHealthy(liquidationLtv)
PM-9	No shares without collateral	totalSupply > 0 implies collateralAmount > 0; skipped after liquidation (collateral can be fully seized while shares remain)
PM-10	Post-liquidation accounting consistency	Checks totalAssets = max(0, quotedCollateral - debt) after liquidation
PM-11	Unauthorized WrappedAsset operations never succeed	Verifies unauthorized transfers and Morpho collateral supply fail

Handler Actions

The PositionManager handler exercises 21 actions:

Category	Actions
Core operations	act_deposit, act_withdraw, act_burn, act_rebalance
Time & fees	act_warpTime, act_setFees, act_accrueInterest
Oracle	act_setOraclePrice
Liquidation	act_preLiquidate, act_morphoLiquidate
Admin	act_setLltv, act_setMaxRebalanceLoss
Morpho	act_supplyMorphoLiquidity, act_morpho_withdraw, act_morpho_repay, act_morpho_supplyCollateral
WrappedAsset	act_wrapped_asset_mint, act_wrapped_asset_burn, act_wrapped_asset_transfer, act_wrapped_asset_approve, act_wrapped_asset_unauthorized_transfer

Facility Invariants

The Facility test suite verifies 10 invariants across 13 handler actions, covering the intent lifecycle, token accounting, and swap mechanics.

ID	Invariant	Verification
FAC-1	Intent state machine is one-way (DEPOSITING → RESOLVING → RESOLVED)	Compares on-chain resolved flag against handler’s tracked state transitions
FAC-2	totalSupply == sum(balances) per intent	Iterates tracked users and sums ERC6909 balances
FAC-3	Deposit/withdraw are 1:1 with LP tokens	Ghost variables capture balance delta vs amount for each deposit/withdraw
FAC-4	Deposit cap never exceeded	Asserts totalSupply(id) <= depositCap for every intent
FAC-5	Token balance solvency — tracked intent balances ≤ actual Facility balances	Aggregates per-intent token amounts (PM shares + debtToken) and compares to real balances
FAC-6	Claim distributes tokens proportionally to shares burned	Ghost variable verifies claimAmount == tokenBalance * shares / totalSupply
FAC-7	Swaps are zero-sum between intents	Captures total token amounts across both intents before/after swap
FAC-8	Swap digest replay prevention	After a successful swap, replays the same signed digest and asserts it reverts
FAC-9	address(0) never holds intent token balance	Checks balanceOf(address(0), id) == 0 for all intents
FAC-10	Pause timestamp consistency	When paused() is true, pausedUntil >= block.timestamp

Handler Actions

The Facility handler exercises 13 actions:

Category	Actions
Intent lifecycle	act_createIntent, act_lock, act_warpToResolving, act_resolve
User operations	act_deposit, act_withdraw, act_claim, act_transfer
Swaps	act_swap
Pause	act_pauseFacility, act_unpauseFacility
Dependencies	act_changeOraclePrice, act_accrueInterest

TransferGuard Invariants

The TransferGuard test suite verifies 6 invariants across 8 handler actions, covering the blocklist/whitelist logic and pause mechanics.

ID	Invariant	Verification
TG-1	BLOCKLIST addresses always blocked	canTransfer returns false for blocklisted as sender or receiver
TG-2	WHITELIST pairs can always transfer	canTransfer returns true for whitelist pairs on non-paused tokens
TG-3	NONE addresses behave per token mode	Allowed in blocklist mode, blocked in whitelist mode
TG-4	Paused token blocks ALL transfers	canTransfer returns false for all pairs when paused
TG-5	Pause expiry consistent with pausedUntil	Verifies pausedUntil == 0 → !paused, expired → !paused, max → paused
TG-6	Permanent pause survives any time warp	pausedUntil == type(uint40).max always means paused() == true

Handler Actions

The TransferGuard handler exercises 8 actions:

Category	Actions
Address management	act_setAddressStatus, act_setAddressStatusBatch
Token config	act_setTokenConfig, act_toggleWhitelistMode
Pause	act_pauseFor, act_unpause, act_permanentPause
Time	act_warpTime

WrappedAsset Invariants

The WrappedAsset test suite verifies 4 invariants across 9 handler actions, covering the 1:1 backing and role-based transfer restrictions.

ID	Invariant	Verification
WA-1	1:1 backing	totalSupply == underlyingToken.balanceOf(wrappedAsset)
WA-2	Transfer restriction enforcement	Unauthorized transfers (no SENDER_ROLE sender, no RECEIVER_ROLE receiver) never succeed
WA-3	ISSUER_ROLE enforcement	mint(to, amount) with to != msg.sender requires ISSUER_ROLE
WA-4	Burn never blocked by role	Burns bypass _beforeTokenTransfer, always succeed regardless of roles

Handler Actions

The WrappedAsset handler exercises 9 actions:

Category	Actions
Core operations	act_mint, act_burn, act_transfer, act_transferFrom, act_approve
Issuer operations	act_mintToOther
Role management	act_grantSenderRole, act_grantReceiverRole, act_revokeRoles

VaultController Fuzz Properties

The VaultController fuzz suite verifies 4 properties using stateless fuzzing:

ID	Property	Verification
REQ-1	Deposit/withdraw round-trip preserves assets	withdraw(deposit(x)) == x for any amount
REQ-2	Share price monotonicity under yield	Share price never decreases after positive yield injection
REQ-3	convertToAssets(convertToShares(x)) ≤ x	Rounding always favors the vault
REQ-4	Total assets = vault balance + deployed	Accounting identity holds after arbitrary deposit/withdraw sequences

Dependency Graph Coverage

The invariant suites exercise cross-contract interactions to verify that state changes in one module cannot create inconsistencies in another:

Dependency	Actions	Affected Suites
Oracle price changes	act_setOraclePrice, act_changeOraclePrice	PM, FAC
Morpho liquidation	act_morphoLiquidate	PM
Pre-liquidation	act_preLiquidate	PM
Interest accrual	act_accrueInterest	PM, FAC
Admin parameter changes	act_setLltv, act_setMaxRebalanceLoss	PM
Morpho liquidity	act_supplyMorphoLiquidity, act_morpho_withdraw	PM
Morpho repay	act_morpho_repay	PM
Unauthorized Morpho ops	act_morpho_supplyCollateral	PM
WrappedAsset wrap/unwrap	act_wrapped_asset_mint, act_wrapped_asset_burn	PM, WA
WrappedAsset transfers	act_wrapped_asset_transfer, act_wrapped_asset_unauthorized_transfer	PM, WA
WrappedAsset role mgmt	act_grantSenderRole, act_grantReceiverRole, act_revokeRoles	WA
Pause/unpause	act_pauseFacility, act_unpauseFacility, act_permanentPause	FAC, TG
Batch operations	act_setAddressStatusBatch	TG
Mode toggling	act_toggleWhitelistMode	TG

Test Configuration

The test configuration in foundry.toml:

# Exclude invariant tests from default runs
no_match_test = "^invariant"

[profile.full]
# Run all tests: FOUNDRY_PROFILE=full forge test
no_match_test = "^$"

[invariant]
runs = 256
depth = 64
fail_on_revert = false

Collateral in the PositionManager and Facility suites uses a real WrappedAsset (ERC1967 proxy) instead of MockERC20, with proper SENDER_ROLE / RECEIVER_ROLE grants to protocol contracts (PM, BorrowPositions, Morpho, Facility).

Liquidation actions (act_preLiquidate, act_morphoLiquidate) call the contracts directly without try/catch, so they revert naturally when positions are healthy — giving visibility into actual liquidation occurrence via the fuzzer’s revert stats.