Merge pull request #5822 from Ratimon/refactor/invariants-burn

contracts-bedrock: Convert Echidna tests  to Forge invariants for Burn library 

packages/contracts-bedrock/contracts/test/invariants/Burn.Eth.t.sol

+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.15;
+
+import { StdUtils } from "forge-std/StdUtils.sol";
+import { Test } from "forge-std/Test.sol";
+import { Vm } from "forge-std/Vm.sol";
+
+import { StdInvariant } from "forge-std/StdInvariant.sol";
+import { Burn } from "../../libraries/Burn.sol";
+
+contract Burn_EthBurner is StdUtils {
+    Vm internal vm;
+    bool public failedEthBurn;
+
+    constructor(Vm _vm) {
+        vm = _vm;
+    }
+
+    /**
+     * @notice Takes an integer amount of eth to burn through the Burn library and
+     * updates the contract state if an incorrect amount of eth moved from the contract
+     */
+    function burnEth(uint256 _value) external {
+        uint256 preBurnvalue = bound(_value, 0, type(uint128).max);
+
+        // Give the burner some ether for gas being used
+        vm.deal(address(this), preBurnvalue);
+
+        // cache the contract's eth balance
+        uint256 preBurnBalance = address(this).balance;
+
+        uint256 value = bound(preBurnvalue, 0, preBurnBalance);
+
+        // execute a burn of _value eth
+        Burn.eth(value);
+
+        // check that exactly value eth was transfered from the contract
+        unchecked {
+            if (address(this).balance != preBurnBalance - value) {
+                failedEthBurn = true;
+            }
+        }
+    }
+}
+
+contract Burn_BurnEth_Invariant is StdInvariant, Test {
+    Burn_EthBurner internal actor;
+
+    function setUp() public {
+        // Create a Eth burner actor.
+
+        actor = new Burn_EthBurner(vm);
+
+        targetContract(address(actor));
+
+        bytes4[] memory selectors = new bytes4[](1);
+        selectors[0] = actor.burnEth.selector;
+        FuzzSelector memory selector = FuzzSelector({ addr: address(actor), selectors: selectors });
+        targetSelector(selector);
+    }
+
+    /**
+     * @custom:invariant `eth(uint256)` always burns the exact amount of eth passed.
+     *
+     * Asserts that when `Burn.eth(uint256)` is called, it always burns the exact amount
+     * of ETH passed to the function.
+     */
+    function invariant_burn_eth() external {
+        // ASSERTION: The amount burned should always match the amount passed exactly
+        assertEq(actor.failedEthBurn(), false);
+    }
+}

packages/contracts-bedrock/contracts/test/invariants/Burn.Gas.t.sol

+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.15;
+
+import { StdUtils } from "forge-std/StdUtils.sol";
+import { Test } from "forge-std/Test.sol";
+import { Vm } from "forge-std/Vm.sol";
+
+import { StdInvariant } from "forge-std/StdInvariant.sol";
+import { Burn } from "../../libraries/Burn.sol";
+
+contract Burn_GasBurner is StdUtils {
+    Vm internal vm;
+    bool public failedGasBurn;
+
+    constructor(Vm _vm) {
+        vm = _vm;
+    }
+
+    /**
+     * @notice Takes an integer amount of gas to burn through the Burn library and
+     * updates the contract state if at least that amount of gas was not burned
+     * by the library
+     */
+    function burnGas(uint256 _value) external {
+        // cap the value to the max resource limit
+        uint256 MAX_RESOURCE_LIMIT = 8_000_000;
+        uint256 value = bound(_value, 0, MAX_RESOURCE_LIMIT);
+
+        // cache the contract's current remaining gas
+        uint256 preBurnGas = gasleft();
+
+        // execute the gas burn
+        Burn.gas(value);
+
+        // cache the remaining gas post burn
+        uint256 postBurnGas = gasleft();
+
+        // check that at least value gas was burnt (and that there was no underflow)
+        unchecked {
+            if (postBurnGas - preBurnGas <= value && preBurnGas - value > preBurnGas) {
+                failedGasBurn = true;
+            }
+        }
+    }
+}
+
+contract Burn_BurnGas_Invariant is StdInvariant, Test {
+    Burn_GasBurner internal actor;
+
+    function setUp() public {
+        // Create a gas burner actor.
+        actor = new Burn_GasBurner(vm);
+
+        targetContract(address(actor));
+
+        bytes4[] memory selectors = new bytes4[](1);
+        selectors[0] = actor.burnGas.selector;
+        FuzzSelector memory selector = FuzzSelector({ addr: address(actor), selectors: selectors });
+        targetSelector(selector);
+    }
+
+    /**
+     * @custom:invariant `gas(uint256)` always burns at least the amount of gas passed.
+     *
+     * Asserts that when `Burn.gas(uint256)` is called, it always burns at least the amount
+     * of gas passed to the function.
+     */
+    function invariant_burn_gas() external {
+        // ASSERTION: The amount burned should always match the amount passed exactly
+        assertEq(actor.failedGasBurn(), false);
+    }
+}

packages/contracts-bedrock/invariant-docs/Burn.Eth.md

+# `Burn.Eth` Invariants
+
+## `eth(uint256)` always burns the exact amount of eth passed.
+**Test:** [`Burn.Eth.t.sol#L68`](../contracts/test/invariants/Burn.Eth.t.sol#L68)
+
+Asserts that when `Burn.eth(uint256)` is called, it always burns the exact amount of ETH passed to the function. 

packages/contracts-bedrock/invariant-docs/Burn.Gas.md

+# `Burn.Gas` Invariants
+
+## `gas(uint256)` always burns at least the amount of gas passed.
+**Test:** [`Burn.Gas.t.sol#L68`](../contracts/test/invariants/Burn.Gas.t.sol#L68)
+
+Asserts that when `Burn.gas(uint256)` is called, it always burns at least the amount of gas passed to the function. 

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

@@ -8,6 +8,8 @@ This directory contains documentation for all defined invariant tests within `co
 ## Table of Contents
 - [AddressAliasHelper](./AddressAliasHelper.md)
 - [AddressAliasing](./AddressAliasing.md)
+- [Burn.Eth](./Burn.Eth.md)
+- [Burn.Gas](./Burn.Gas.md)
 - [Burn](./Burn.md)
 - [CrossDomainMessenger](./CrossDomainMessenger.md)
 - [Encoding](./Encoding.md)