​
Use Case

Check that protocols maintain proper security controls during emergency pause states. When a protocol enters a panic/pause state, it’s critical to ensure that:

  • No new deposits can be made to the protocol
  • Existing users can still withdraw their funds
  • Protocol state changes are restricted to emergency operations only
  • No unauthorized state modifications occur during the pause

This assertion is particularly important because:

  • Emergency pause mechanisms are a critical security feature for DeFi protocols
  • Improper handling of pause states can lead to fund lockups or unauthorized access
  • Many high-profile hacks have been prevented by proper pause mechanisms
  • Users need confidence they can exit during emergencies

​
Applicable Protocols

  • Yield aggregators and vaults (e.g., Yearn, Beefy)
  • Lending protocols with pause mechanisms
  • DEXs with emergency circuit breakers
  • Cross-chain bridges with pause functionality
  • Any protocol with emergency pause capabilities

These protocols particularly need this assertion because:

  • They often hold significant user funds
  • They have complex state transitions that must be restricted during emergencies
  • Users need guaranteed withdrawal capabilities during crises
  • Protocol upgrades or maintenance should be blocked during pause states

​
Explanation

The assertion monitors the protocol’s balance and pause state to ensure proper behavior during emergencies. It uses a multi-layered approach:

  1. First, it checks if the protocol is in a paused state
  2. If paused, it verifies that the protocol’s balance can only decrease (allowing withdrawals)
  3. It uses state change tracking to detect any unauthorized modifications

The assertion uses the following cheatcodes and functions:

  • ph.forkPreState(): Captures the initial state before the transaction
  • ph.forkPostState(): Captures the final state after the transaction
  • getStateChangesUint(): Tracks all state changes during the transaction
  • registerCallTrigger(): Monitors all function calls to the contract

This approach ensures that:

  1. Users can always withdraw their funds during emergencies
  2. No new deposits can be made while paused
  3. Protocol state remains consistent during pause periods

For more information about cheatcodes, see the Cheatcodes Documentation.

Note: In the future, this assertion could be optimized with a new trigger type that only fires when a specific storage slot has a specific value (e.g., when the pause flag is true). This would reduce unnecessary assertion checks and improve efficiency.

​
Code Example

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.13;

import {Assertion} from "credible-std/Assertion.sol";
import {PhEvm} from "credible-std/PhEvm.sol";

interface IEmergencyPausable {
    function paused() external view returns (bool);
    function balance() external view returns (uint256);
}

contract EmergencyStateAssertion is Assertion {
    IEmergencyPausable public vault;

    constructor(address vault_) {
        vault = IEmergencyPausable(vault_);
    }

    function triggers() external view override {
        // Register trigger for all function calls to ensure comprehensive coverage
        registerCallTrigger(this.assertionPanickedCanOnlyDecreaseBalance.selector);
    }

    // Check that if the state is panicked that the pool balance can only decrease
    // This ensures users can withdraw but prevents new deposits
    function assertionPanickedCanOnlyDecreaseBalance() external {
        // Get pre-state values
        ph.forkPreState();
        bool isPanicked = vault.paused();
        uint256 preBalance = vault.balance();

        // Get post-state values
        ph.forkPostState();
        uint256 postBalance = vault.balance();

        // If protocol is paused, ensure balance can only decrease
        if (isPanicked) {
            require(postBalance <= preBalance, "Balance can only decrease when panicked");

            // Additional check: verify no unauthorized state changes
            uint256[] memory changes = getStateChangesUint(
                address(vault),
                bytes32(uint256(1)) // Balance storage slot, change according to your contract
            );

            // Ensure all intermediate states maintain the decrease-only property
            for (uint256 i = 0; i < changes.length; i++) {
                require(changes[i] <= preBalance, "Unauthorized state change during pause");
            }
        }
    }
}

Note: This code example is maintained in the Phylax Assertion Examples Repository. For a full examples with mock protocol code and tests please refer to the repository.

​
Testing

To test this assertion:

  1. Deploy the assertion contract with a test vault
  2. Set up test scenarios:
    • Normal operation (not paused)
    • Paused state with withdrawals
    • Paused state with attempted deposits
    • Paused state with multiple state changes in a single transaction
  3. Verify the assertion correctly:
    • Allows balance decreases during pause
    • Blocks balance increases during pause
    • Maintains proper state during complex transactions

​
Assertion Best Practices

  • Combine with other assertions like Owner Change for comprehensive security
  • Use getStateChangesUint to detect unauthorized modifications throughout the call stack during pause states
  • Consider adding whitelisted addresses that can modify state during emergencies (e.g. for upgrades or liquidity management)
  • Implement proper error messages to help with debugging