From Invariant to Assertion

This guide walks you through the process of turning a protocol invariant into a working assertion. By the end, you’ll understand how to identify invariants, handle exceptions, and write assertion code that protects your protocol. Prerequisites: Familiarity with Solidity, the Assertions Overview, and the Assertion Guide. What you’ll build: An assertion that protects vault share prices in Euler’s Vault Kit. Throughout this guide, we’ll use a real example: protecting vault share prices in Euler’s Ethereum Vault Connector (EVC). This example demonstrates the full journey from protocol specification to working assertion. The invariant we’ll implement:

“A vault’s share price should not decrease unless bad debt socialization occurs.”

This protects depositors from economic attacks, protocol bugs, and malicious vault implementations while allowing legitimate protocol operations.

Step 1: Find and Define the Invariant

Where Do Invariants Come From?

Invariants typically come from:

Protocol specifications and whitepapers: The authoritative source for how the protocol should behave
Security audits: Often document critical properties that must hold
Your own analysis: Asking “what should never happen?”

For our example, the Euler Vault Kit specification defines how vaults should behave. A fundamental property of any vault is that share prices should be stable or increasing over time as yield accrues.

Define the Invariant

Start by asking: What should never happen? For a vault, a decreasing share price means depositors are losing value. In pseudo-Solidity:

// What we want to enforce
require(sharePriceAfter >= sharePriceBefore, "Share price decreased");

This is our starting invariant. But before we implement it, we need to check for legitimate exceptions.

Step 2: Identify Exceptions

Not every invariant violation is an attack. Protocol specifications often document legitimate scenarios where an invariant might not hold.

Bad Debt Socialization

The Euler Vault Kit whitepaper describes a scenario called “bad debt socialization”:

When an account in violation has had all of its collateral seized during a liquidation but still has a non-zero liability, this liability is called bad debt and is cancelled, socialising the loss to all current depositors in the vault.

This is an intentional design decision to avoid bank-run scenarios. When bad debt is socialized, the share price decreases, but this is expected behavior, not an attack. The whitepaper also specifies how this is signaled:

To allow off-chain users to accurately track total borrows and internal balances using event logs, bad debt socialisation emits Repay and Withdraw logs, where the repay appears to come from the liquidator and the withdraw appears to come from address(0).

Refine the Invariant

Now we can refine our invariant to account for this exception:

// Refined invariant
require(
    sharePriceAfter >= sharePriceBefore || badDebtSocialized,
    "Share price decreased without bad debt socialization"
);

In plain English: “Share price cannot decrease unless bad debt socialization occurs.”

Always check protocol specifications for documented exceptions before implementing an invariant. What looks like an attack might be intentional behavior.

Step 3: Determine Where to Enforce

Before writing code, decide where to check the invariant. You have two options:

At each vault individually: Check share price on every vault contract
At a central entry point: Check share price at the contract that routes calls to vaults

For Euler, the EVC (Ethereum Vault Connector) is the central entry point for all vault interactions. Users don’t call vaults directly; they go through the EVC’s batch(), call(), and controlCollateral() functions. Why check at the EVC?

Single assertion covers all vaults
Catches attacks regardless of which vault is targeted
Simpler to maintain than per-vault assertions

This is a common pattern: find the chokepoint where all relevant transactions flow, and enforce your invariant there.

Step 4: Choose Your Triggers

Now we need to specify when our assertion should run. Looking at the EVC interface, three functions can lead to vault interactions:

batch(): Execute multiple operations atomically
call(): Execute a single operation on a target contract
controlCollateral(): Manage collateral positions

We register a trigger for each:

function triggers() external view override {
    registerFnCallTrigger(this.assertionBatchSharePriceInvariant.selector, IEVC.batch.selector);
    registerFnCallTrigger(this.assertionCallSharePriceInvariant.selector, IEVC.call.selector);
    registerFnCallTrigger(this.assertionControlCollateralSharePriceInvariant.selector, IEVC.controlCollateral.selector);
}

Each trigger maps an EVC function to an assertion function that will validate the invariant. See Triggers for more information.

Step 5: Write the Assertion Logic

Now we implement the assertion. We’ll break this into three parts:

Part A: Get the Vault Address

For each entry point, we need to extract which vault is being interacted with. Here’s how we do it for call():

function assertionCallSharePriceInvariant() external {
    IEVC evc = IEVC(ph.getAssertionAdopter());
    
    // Get all calls to the EVC's call() function
    PhEvm.CallInputs[] memory calls = ph.getCallInputs(address(evc), IEVC.call.selector);
    
    for (uint256 i = 0; i < calls.length; i++) {
        // Decode to get the target vault address
        (address targetContract,,,) = abi.decode(calls[i].input, (address, address, uint256, bytes));
        
        // Validate share price for this vault
        validateVaultSharePriceInvariant(targetContract);
    }
}

Cheatcodes used:

ph.getAssertionAdopter(): Get the contract address this assertion is protecting
ph.getCallInputs(): Get all calls to a specific function

The core logic compares share prices before and after the transaction:

function validateVaultSharePriceInvariant(address vault) internal view {
    // Skip non-contract addresses
    if (vault.code.length == 0) return;

    PhEvm.ForkId memory preTx = _preTx();
    PhEvm.ForkId memory postTx = _postTx();

    uint256 preSharePrice = getSharePriceAt(vault, preTx);
    uint256 postSharePrice = getSharePriceAt(vault, postTx);
    
    // Check the invariant
    if (postSharePrice < preSharePrice) {
        bool hasLegitimateBadDebt = checkForBadDebtSocialization(vault);
        
        require(
            hasLegitimateBadDebt,
            "Share price decreased without bad debt socialization"
        );
    }
}

function getSharePriceAt(address vault, PhEvm.ForkId memory fork) internal view returns (uint256) {
    uint256 totalAssets = uint256(ph.loadStateAt(vault, TOTAL_ASSETS_SLOT, fork));
    uint256 totalSupply = uint256(ph.loadStateAt(vault, TOTAL_SUPPLY_SLOT, fork));
    
    if (totalSupply > 0) {
        return (totalAssets * 1e18) / totalSupply;
    }
    return 0;
}

Cheatcodes used:

PhEvm.ForkId: Identifies the pre-transaction and post-transaction snapshots
ph.loadStateAt(): Reads a storage slot at a specific snapshot

Part C: Detect Bad Debt Socialization

Finally, we check if a share price decrease is due to legitimate bad debt socialization:

function checkForBadDebtSocialization(address vault) internal returns (bool) {
    PhEvm.Log[] memory logs = ph.getLogs();
    
    bool hasDebtSocializedEvent = false;
    bool hasRepayFromLiquidator = false;
    bool hasWithdrawFromZero = false;
    
    for (uint256 i = 0; i < logs.length; i++) {
        if (logs[i].emitter != vault) continue;
        
        // Check for DebtSocialized event (added after whitepaper)
        if (logs[i].topics[0] == keccak256("DebtSocialized(address,uint256)")) {
            hasDebtSocializedEvent = true;
        }
        
        // Check for Repay event from liquidator (per whitepaper spec)
        if (logs[i].topics[0] == keccak256("Repay(address,uint256)")) {
            address account = address(uint160(uint256(logs[i].topics[1])));
            if (account != address(0)) {
                hasRepayFromLiquidator = true;
            }
        }
        
        // Check for Withdraw from address(0) (per whitepaper spec)
        if (logs[i].topics[0] == keccak256("Withdraw(address,address,address,uint256,uint256)")) {
            address sender = address(uint160(uint256(logs[i].topics[1])));
            if (sender == address(0)) {
                hasWithdrawFromZero = true;
            }
        }
    }
    
    // Bad debt detected via new event OR legacy pattern from whitepaper
    return hasDebtSocializedEvent || (hasRepayFromLiquidator && hasWithdrawFromZero);
}

Cheatcodes used:

ph.getLogs(): Retrieve all logs emitted during the transaction

We check for both the DebtSocialized event (added after the whitepaper was written) and the original Repay + Withdraw pattern documented in the spec. This defensive approach ensures we catch bad debt socialization even if there’s an edge case where the new event isn’t emitted.

View the complete assertion contract to see how all these pieces fit together.

Step 6: Test Your Assertion

Before deploying, you should thoroughly test your assertion. Here are the three most common test cases for this invariant:

Normal operation: Share price increases or stays the same (should pass)
Attack scenario: Share price decreases without bad debt (should fail)
Legitimate exception: Share price decreases with bad debt socialization (should pass)

Here are concrete test examples using the call() entry point. Tests use cl.assertion() to register the assertion before executing the transaction.

Test 1: Normal Operation (Should Pass)

function testVaultSharePriceAssertion_SingleCall_Passes() public {
    // Setup vault with initial state
    token1.mint(address(vault1), 1000e18);
    vault1.setTotalAssets(1000e18);
    vault1.mint(1000e18, user1); // Share price = 1.0

    // Register assertion
    cl.assertion({
        adopter: address(evc),
        createData: type(VaultSharePriceAssertion).creationCode,
        fnSelector: VaultSharePriceAssertion.assertionCallSharePriceInvariant.selector
    });

    // Execute call that increases share price
    vm.prank(user1);
    evc.call(
        address(vault1),
        user1,
        0,
        abi.encodeWithSelector(MockERC4626Vault.increaseSharePrice.selector, 100e18)
    );

    // Assertion passes - share price increased
}

Test 2: Attack Detection (Should Fail)

function testVaultSharePriceAssertion_SingleCall_Fails() public {
    // Setup vault with initial state
    token1.mint(address(vault1), 1000e18);
    vault1.setTotalAssets(1000e18);
    vault1.mint(1000e18, user1);

    // Register assertion
    cl.assertion({
        adopter: address(evc),
        createData: type(VaultSharePriceAssertion).creationCode,
        fnSelector: VaultSharePriceAssertion.assertionCallSharePriceInvariant.selector
    });

    // Execute call that decreases share price WITHOUT bad debt
    vm.prank(user1);
    vm.expectRevert("VaultSharePriceAssertion: Share price decreased without bad debt socialization");
    evc.call(
        address(vault1),
        user1,
        0,
        abi.encodeWithSelector(MockERC4626Vault.decreaseSharePrice.selector, 100e18)
    );
}

Test 3: Legitimate Exception (Should Pass)

function testVaultSharePriceAssertion_SharePriceDecreaseWithBadDebt_Passes() public {
    // Setup vault with initial state
    token1.mint(address(vault1), 1000e18);
    vault1.setTotalAssets(1000e18);
    vault1.mint(1000e18, user1);

    // Register assertion
    cl.assertion({
        adopter: address(evc),
        createData: type(VaultSharePriceAssertion).creationCode,
        fnSelector: VaultSharePriceAssertion.assertionCallSharePriceInvariant.selector
    });

    // Execute call that decreases share price WITH bad debt socialization events
    vm.prank(user1);
    evc.call(
        address(vault1),
        user1,
        0,
        abi.encodeWithSelector(MockERC4626Vault.decreaseSharePriceWithBadDebt.selector, 100e18)
    );

    // Assertion passes - bad debt socialization detected
}

These are basic sanity checks. For production assertions, test edge cases like zero total supply, non-ERC4626 contracts, and zero addresses. Your assertion should handle these gracefully without reverting unexpectedly.

See the full test file for the complete test suite covering all entry points and edge cases. For thorough testing guidance including fuzz testing and backtesting against historical transactions, see Testing Assertions, Fuzz Testing, and Backtesting.

Recap

You’ve learned the process of turning an invariant into an assertion:

Find the invariant: Check protocol specs, whitepapers, and audits
Identify exceptions: Not every violation is an attack
Determine where to enforce: Find the chokepoint where transactions flow
Choose triggers: Specify which functions should invoke your assertion
Write the logic: Use cheatcodes to compare pre/post state and handle exceptions
Test thoroughly: Verify normal operations pass and attacks are caught

The complete example from this guide is available in our fork of the EVC repository.

Next Steps

Assertions Book

More real-world assertion examples

Cheatcodes Reference

Complete reference for assertion cheatcodes

Testing Assertions

How to test your assertions

Triggers

Learn about trigger types and optimization

Start Here

Tutorials

How-to Guides

Explanation

Platform

Reference

Step 1: Find and Define the Invariant

Where Do Invariants Come From?

Define the Invariant

Step 2: Identify Exceptions

Bad Debt Socialization

Refine the Invariant

Step 3: Determine Where to Enforce

Step 4: Choose Your Triggers

Step 5: Write the Assertion Logic

Part A: Get the Vault Address

Part C: Detect Bad Debt Socialization

Step 6: Test Your Assertion

Test 1: Normal Operation (Should Pass)

Test 2: Attack Detection (Should Fail)

Test 3: Legitimate Exception (Should Pass)

Recap

Next Steps

Assertions Book

Cheatcodes Reference

Testing Assertions

Triggers

​The Example: Euler Vault Share Price

​Step 1: Find and Define the Invariant

​Where Do Invariants Come From?

​Define the Invariant

​Step 2: Identify Exceptions

​Bad Debt Socialization

​Refine the Invariant

​Step 3: Determine Where to Enforce

​Step 4: Choose Your Triggers

​Step 5: Write the Assertion Logic

​Part A: Get the Vault Address

​Part B: Compare Pre and Post Share Price

​Part C: Detect Bad Debt Socialization

​Step 6: Test Your Assertion

​Test 1: Normal Operation (Should Pass)

​Test 2: Attack Detection (Should Fail)

​Test 3: Legitimate Exception (Should Pass)

​Recap

​Next Steps

Assertions Book

Cheatcodes Reference

Testing Assertions

Triggers

The Example: Euler Vault Share Price

Step 1: Find and Define the Invariant

Where Do Invariants Come From?

Define the Invariant

Step 2: Identify Exceptions

Bad Debt Socialization

Refine the Invariant

Step 3: Determine Where to Enforce

Step 4: Choose Your Triggers

Step 5: Write the Assertion Logic

Part A: Get the Vault Address

Part B: Compare Pre and Post Share Price

Part C: Detect Bad Debt Socialization

Step 6: Test Your Assertion

Test 1: Normal Operation (Should Pass)

Test 2: Attack Detection (Should Fail)

Test 3: Legitimate Exception (Should Pass)

Recap

Next Steps