Merge pull request #5985 from Ratimon/refactor/invariants-resource-metering

contracts-bedrock: Convert Echidna tests to Forge invariants for ResourceMetering

packages/contracts-bedrock/contracts/test/invariants/ResourceMetering.t.sol

+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.15;
+
+import { Test } from "forge-std/Test.sol";
+
+import { StdUtils } from "forge-std/StdUtils.sol";
+import { StdInvariant } from "forge-std/StdInvariant.sol";
+
+import { Arithmetic } from "../../libraries/Arithmetic.sol";
+import { ResourceMetering } from "../../L1/ResourceMetering.sol";
+import { Proxy } from "../../universal/Proxy.sol";
+import { Constants } from "../../libraries/Constants.sol";
+
+contract ResourceMetering_User is StdUtils, ResourceMetering {
+    bool public failedMaxGasPerBlock;
+    bool public failedRaiseBaseFee;
+    bool public failedLowerBaseFee;
+    bool public failedNeverBelowMinBaseFee;
+    bool public failedMaxRaiseBaseFeePerBlock;
+    bool public failedMaxLowerBaseFeePerBlock;
+
+    // Used as a special flag for the purpose of identifying unchecked math errors specifically
+    // in the test contracts, not the target contracts themselves.
+    bool public underflow;
+
+    constructor() {
+        initialize();
+    }
+
+    function initialize() internal initializer {
+        __ResourceMetering_init();
+    }
+
+    function resourceConfig() public pure returns (ResourceMetering.ResourceConfig memory) {
+        return _resourceConfig();
+    }
+
+    function _resourceConfig()
+        internal
+        pure
+        override
+        returns (ResourceMetering.ResourceConfig memory)
+    {
+        ResourceMetering.ResourceConfig memory rcfg = Constants.DEFAULT_RESOURCE_CONFIG();
+        return rcfg;
+    }
+
+    /**
+     * @notice Takes the necessary parameters to allow us to burn arbitrary amounts of gas to test
+     *         the underlying resource metering/gas market logic
+     */
+    function burn(uint256 _gasToBurn, bool _raiseBaseFee) public {
+        // Part 1: we cache the current param values and do some basic checks on them.
+        uint256 cachedPrevBaseFee = uint256(params.prevBaseFee);
+        uint256 cachedPrevBoughtGas = uint256(params.prevBoughtGas);
+        uint256 cachedPrevBlockNum = uint256(params.prevBlockNum);
+
+        ResourceMetering.ResourceConfig memory rcfg = resourceConfig();
+        uint256 targetResourceLimit = uint256(rcfg.maxResourceLimit) /
+            uint256(rcfg.elasticityMultiplier);
+
+        // check that the last block's base fee hasn't dropped below the minimum
+        if (cachedPrevBaseFee < uint256(rcfg.minimumBaseFee)) {
+            failedNeverBelowMinBaseFee = true;
+        }
+        // check that the last block didn't consume more than the max amount of gas
+        if (cachedPrevBoughtGas > uint256(rcfg.maxResourceLimit)) {
+            failedMaxGasPerBlock = true;
+        }
+
+        // Part2: we perform the gas burn
+
+        // force the gasToBurn into the correct range based on whether we intend to
+        // raise or lower the baseFee after this block, respectively
+        uint256 gasToBurn;
+        if (_raiseBaseFee) {
+            gasToBurn = bound(
+                _gasToBurn,
+                uint256(targetResourceLimit),
+                uint256(rcfg.maxResourceLimit)
+            );
+        } else {
+            gasToBurn = bound(_gasToBurn, 0, targetResourceLimit);
+        }
+
+        _burnInternal(uint64(gasToBurn));
+
+        // Part 3: we run checks and modify our invariant flags based on the updated params values
+
+        // Calculate the maximum allowed baseFee change (per block)
+        uint256 maxBaseFeeChange = cachedPrevBaseFee / uint256(rcfg.baseFeeMaxChangeDenominator);
+
+        // If the last block used more than the target amount of gas (and there were no
+        // empty blocks in between), ensure this block's baseFee increased, but not by
+        // more than the max amount per block
+        if (
+            (cachedPrevBoughtGas > uint256(targetResourceLimit)) &&
+            (uint256(params.prevBlockNum) - cachedPrevBlockNum == 1)
+        ) {
+            failedRaiseBaseFee = failedRaiseBaseFee || (params.prevBaseFee <= cachedPrevBaseFee);
+            failedMaxRaiseBaseFeePerBlock =
+                failedMaxRaiseBaseFeePerBlock ||
+                ((uint256(params.prevBaseFee) - cachedPrevBaseFee) < maxBaseFeeChange);
+        }
+
+        // If the last block used less than the target amount of gas, (or was empty),
+        // ensure that: this block's baseFee was decreased, but not by more than the max amount
+        if (
+            (cachedPrevBoughtGas < uint256(targetResourceLimit)) ||
+            (uint256(params.prevBlockNum) - cachedPrevBlockNum > 1)
+        ) {
+            // Invariant: baseFee should decrease
+            failedLowerBaseFee =
+                failedLowerBaseFee ||
+                (uint256(params.prevBaseFee) > cachedPrevBaseFee);
+
+            if (params.prevBlockNum - cachedPrevBlockNum == 1) {
+                // No empty blocks
+                // Invariant: baseFee should not have decreased by more than the maximum amount
+                failedMaxLowerBaseFeePerBlock =
+                    failedMaxLowerBaseFeePerBlock ||
+                    ((cachedPrevBaseFee - uint256(params.prevBaseFee)) <= maxBaseFeeChange);
+            } else if (params.prevBlockNum - cachedPrevBlockNum > 1) {
+                // We have at least one empty block
+                // Update the maxBaseFeeChange to account for multiple blocks having passed
+                unchecked {
+                    maxBaseFeeChange = uint256(
+                        int256(cachedPrevBaseFee) -
+                            Arithmetic.clamp(
+                                Arithmetic.cdexp(
+                                    int256(cachedPrevBaseFee),
+                                    int256(uint256(rcfg.baseFeeMaxChangeDenominator)),
+                                    int256(uint256(params.prevBlockNum) - cachedPrevBlockNum)
+                                ),
+                                int256(uint256(rcfg.minimumBaseFee)),
+                                int256(uint256(rcfg.maximumBaseFee))
+                            )
+                    );
+                }
+
+                // Detect an underflow in the previous calculation.
+                // Without using unchecked above, and detecting the underflow here, fuzzer would
+                // otherwise ignore the revert.
+                underflow = underflow || maxBaseFeeChange > cachedPrevBaseFee;
+
+                // Invariant: baseFee should not have decreased by more than the maximum amount
+                failedMaxLowerBaseFeePerBlock =
+                    failedMaxLowerBaseFeePerBlock ||
+                    ((cachedPrevBaseFee - uint256(params.prevBaseFee)) <= maxBaseFeeChange);
+            }
+        }
+    }
+
+    function _burnInternal(uint64 _gasToBurn) private metered(_gasToBurn) {}
+}
+
+contract ResourceMetering_Invariant is StdInvariant, Test {
+    ResourceMetering_User internal actor;
+
+    function setUp() public {
+        // Create a actor.
+        actor = new ResourceMetering_User();
+
+        targetContract(address(actor));
+
+        bytes4[] memory selectors = new bytes4[](1);
+        selectors[0] = actor.burn.selector;
+        FuzzSelector memory selector = FuzzSelector({ addr: address(actor), selectors: selectors });
+        targetSelector(selector);
+    }
+
+    /**
+     * @custom:invariant The base fee should increase if the last block used more
+     * than the target amount of gas
+     *
+     * If the last block used more than the target amount of gas (and there were no
+     * empty blocks in between), ensure this block's baseFee increased, but not by
+     * more than the max amount per block.
+     */
+    function invariant_high_usage_raise_baseFee() external {
+        assertFalse(actor.failedRaiseBaseFee());
+    }
+
+    /**
+     * @custom:invariant The base fee should decrease if the last block used less
+     * than the target amount of gas
+     *
+     * If the previous block used less than the target amount of gas, the base fee should decrease,
+     * but not more than the max amount.
+     */
+    function invariant_low_usage_lower_baseFee() external {
+        assertFalse(actor.failedLowerBaseFee());
+    }
+
+    /**
+     * @custom:invariant A block's base fee should never be below `MINIMUM_BASE_FEE`
+     *
+     * This test asserts that a block's base fee can never drop below the
+     * `MINIMUM_BASE_FEE` threshold.
+     */
+    function invariant_never_below_min_baseFee() external {
+        assertFalse(actor.failedNeverBelowMinBaseFee());
+    }
+
+    /**
+     * @custom:invariant A block can never consume more than `MAX_RESOURCE_LIMIT` gas.
+     *
+     * This test asserts that a block can never consume more than the `MAX_RESOURCE_LIMIT`
+     * gas threshold.
+     */
+    function invariant_never_above_max_gas_limit() external {
+        assertFalse(actor.failedMaxGasPerBlock());
+    }
+
+    /**
+     * @custom:invariant The base fee can never be raised more than the max base fee change.
+     *
+     * After a block consumes more gas than the target gas, the base fee cannot be raised
+     * more than the maximum amount allowed. The max base fee change (per-block) is derived
+     * as follows: `prevBaseFee / BASE_FEE_MAX_CHANGE_DENOMINATOR`
+     */
+    function invariant_never_exceed_max_increase() external {
+        assertFalse(actor.failedMaxRaiseBaseFeePerBlock());
+    }
+
+    /**
+     * @custom:invariant The base fee can never be lowered more than the max base fee change.
+     *
+     * After a block consumes less than the target gas, the base fee cannot be lowered more
+     * than the maximum amount allowed. The max base fee change (per-block) is derived as
+     *follows: `prevBaseFee / BASE_FEE_MAX_CHANGE_DENOMINATOR`
+     */
+    function invariant_never_exceed_max_decrease() external {
+        assertFalse(actor.failedMaxLowerBaseFeePerBlock());
+    }
+
+    /**
+     * @custom:invariant The `maxBaseFeeChange` calculation over multiple blocks can never
+     * underflow.
+     *
+     * When calculating the `maxBaseFeeChange` after multiple empty blocks, the calculation
+     * should never be allowed to underflow.
+     */
+    function invariant_never_underflow() external {
+        assertFalse(actor.underflow());
+    }
+}

packages/contracts-bedrock/invariant-docs/ResourceMetering.md

 # `ResourceMetering` Invariants
 
+## The base fee should increase if the last block used more than the target amount of gas
+**Test:** [`ResourceMetering.t.sol#L180`](../contracts/test/invariants/ResourceMetering.t.sol#L180)
+
+If the last block used more than the target amount of gas (and there were no empty blocks in between), ensure this block's baseFee increased, but not by more than the max amount per block. 
+
+
+## The base fee should decrease if the last block used less than the target amount of gas
+**Test:** [`ResourceMetering.t.sol#L191`](../contracts/test/invariants/ResourceMetering.t.sol#L191)
+
+If the previous block used less than the target amount of gas, the base fee should decrease, but not more than the max amount. 
+
+
+## A block's base fee should never be below `MINIMUM_BASE_FEE`
+**Test:** [`ResourceMetering.t.sol#L201`](../contracts/test/invariants/ResourceMetering.t.sol#L201)
+
+This test asserts that a block's base fee can never drop below the `MINIMUM_BASE_FEE` threshold. 
+
+
+## A block can never consume more than `MAX_RESOURCE_LIMIT` gas.
+**Test:** [`ResourceMetering.t.sol#L211`](../contracts/test/invariants/ResourceMetering.t.sol#L211)
+
+This test asserts that a block can never consume more than the `MAX_RESOURCE_LIMIT` gas threshold. 
+
+
+## The base fee can never be raised more than the max base fee change.
+**Test:** [`ResourceMetering.t.sol#L222`](../contracts/test/invariants/ResourceMetering.t.sol#L222)
+
+After a block consumes more gas than the target gas, the base fee cannot be raised more than the maximum amount allowed. The max base fee change (per-block) is derived as follows: `prevBaseFee / BASE_FEE_MAX_CHANGE_DENOMINATOR` 
+
+
+## The base fee can never be lowered more than the max base fee change.
+**Test:** [`ResourceMetering.t.sol#L233`](../contracts/test/invariants/ResourceMetering.t.sol#L233)
+
+After a block consumes less than the target gas, the base fee cannot be lowered more than the maximum amount allowed. The max base fee change (per-block) is derived as follows: `prevBaseFee / BASE_FEE_MAX_CHANGE_DENOMINATOR` 
+
+
+## The `maxBaseFeeChange` calculation over multiple blocks can never underflow.
+**Test:** [`ResourceMetering.t.sol#L244`](../contracts/test/invariants/ResourceMetering.t.sol#L244)
+
+When calculating the `maxBaseFeeChange` after multiple empty blocks, the calculation should never be allowed to underflow. 
+
+
 ## The base fee should increase if the last block used more than the target amount of gas
 **Test:** [`FuzzResourceMetering.sol#L158`](../contracts/echidna/FuzzResourceMetering.sol#L158)