Implementation Address Change - Phylax Credible Layer Documentation

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.

​When to Use This Pattern

​What This Pattern Checks

​Assertion Pattern

​Related Patterns

When to Use This Pattern

What This Pattern Checks

Assertion Pattern

Related Patterns