Modified Key Discovery

function changedMappingKeys(
    address target,
    bytes32 baseSlot
) external view returns (bytes[] memory keys);

function mappingValueDiff(
    address target,
    bytes32 baseSlot,
    bytes calldata key,
    uint256 fieldOffset
) external view returns (bytes32 pre, bytes32 post, bool changed);

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

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

contract ModifiedBalanceAssertion is Assertion {
    bytes32 internal constant BALANCES_SLOT = bytes32(uint256(0));
    uint256 internal immutable MAX_BALANCE;

    constructor(uint256 maxBalance_) {
        MAX_BALANCE = maxBalance_;
        registerAssertionSpec(AssertionSpec.Reshiram);
    }

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

    function assertModifiedBalances() external view {
        address target = ph.getAssertionAdopter();
        bytes[] memory keys = ph.changedMappingKeys(target, BALANCES_SLOT);

        for (uint256 i = 0; i < keys.length; i++) {
            (, bytes32 afterValue, bool changed) =
                ph.mappingValueDiff(target, BALANCES_SLOT, keys[i], 0);

            if (!changed) continue;
            require(uint256(afterValue) <= MAX_BALANCE, "balance exceeds limit");
        }
    }
}