Skip to main content

Documentation Index

Fetch the complete documentation index at: https://docs.phylax.systems/llms.txt

Use this file to discover all available pages before exploring further.

​
When to Use This Pattern

Ensures protocols maintain proper security controls during emergency pause states, allowing existing users to withdraw funds while preventing new deposits. Critical for yield aggregators and vaults (Yearn, Beefy), lending protocols with pause mechanisms, DEXs with emergency circuit breakers, cross-chain bridges with pause functionality, and any protocol with emergency pause capabilities. Improper handling of pause states can lead to fund lockups, unauthorized access, or users being unable to exit during emergencies.

​
What This Pattern Checks

Monitors protocol balance and pause state to ensure proper emergency behavior using a multi-layered approach:
  • _preTx() / _postTx() with Reshiram snapshot reads: Capture protocol state before and after transaction
  • ph.loadStateAt(): Read the pause and balance slots at pre-transaction and post-transaction snapshots
  • registerFnCallTrigger(): Monitor all function calls to the contract
  • Verify protocol balance can only decrease when paused (allowing withdrawals)
  • Detect unauthorized modifications during pause periods
The assertion ensures users can withdraw funds during emergencies while preventing new deposits and maintaining protocol state consistency.
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.
For more information about cheatcodes, see the Cheatcodes Documentation.

​
Assertion Pattern

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

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

contract EmergencyStateAssertion is Assertion {
    bytes32 internal constant PAUSED_SLOT = bytes32(uint256(0));
    bytes32 internal constant BALANCE_SLOT = bytes32(uint256(1));

    constructor() {
        registerAssertionSpec(AssertionSpec.Reshiram);
    }

    function triggers() external view override {
        registerTxEndTrigger(this.assertionPanickedCanOnlyDecreaseBalance.selector);
    }

    /// @notice Checks that a paused protocol cannot increase its stored balance.
    function assertionPanickedCanOnlyDecreaseBalance() external view {
        address adopter = ph.getAssertionAdopter();
        PhEvm.ForkId memory preFork = _preTx();
        PhEvm.ForkId memory postFork = _postTx();

        bool wasPaused = uint256(ph.loadStateAt(adopter, PAUSED_SLOT, preFork)) != 0;
        if (!wasPaused) {
            return;
        }

        uint256 preBalance = uint256(ph.loadStateAt(adopter, BALANCE_SLOT, preFork));
        uint256 postBalance = uint256(ph.loadStateAt(adopter, BALANCE_SLOT, postFork));

        require(postBalance <= preBalance, "Balance can only decrease when panicked");
    }
}
Full examples and mock protocol code are available in credible-std.