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

Prevents unauthorized changes to proxy implementation addresses, which could allow attackers to replace contract logic with malicious code. Critical for proxy-based upgradeable contracts in DeFi protocols (lending pools, yield aggregators), governance systems with timelocks, and cross-chain bridges. For example, it’s possible to define a whitelist of allowed implementations - any other implementation would be considered an invalid state.

​
What This Pattern Checks

Monitors changes to the implementation address storage slot in proxy contracts using:
  • _preTx() / _postTx() with Reshiram snapshot reads: Compare implementation address before and after transaction
  • ph.loadStateAt(): Load the implementation slot at each snapshot
  • registerTxEndTrigger(): Trigger when implementation address changes
The assertion performs a direct pre/post comparison of the protected implementation slot. 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 ImplementationChangeAssertion is Assertion {
    bytes32 internal constant IMPLEMENTATION_SLOT = bytes32(uint256(0));

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

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

    /// @notice Checks that the implementation slot is unchanged across the transaction.
    function implementationChange() external view {
        address adopter = ph.getAssertionAdopter();
        PhEvm.ForkId memory preFork = _preTx();
        PhEvm.ForkId memory postFork = _postTx();

        address preImpl = _loadAddressAt(adopter, IMPLEMENTATION_SLOT, preFork);
        address postImpl = _loadAddressAt(adopter, IMPLEMENTATION_SLOT, postFork);

        require(preImpl == postImpl, "Implementation changed");
    }

    function _loadAddressAt(address target, bytes32 slot, PhEvm.ForkId memory fork) internal view returns (address) {
        return address(uint160(uint256(ph.loadStateAt(target, slot, fork))));
    }
}
Full examples and mock protocol code are available in credible-std.