contracts-bedrock: Convert Echidna tests to Forge invariants for OptimismPortal (#5852)

* Refactor: Adding tests for Portal contract

* Fix linting

* Doc: auto-gen doc for invariant

* Fix : Adding try & catch
Co-authored-by: clabby <ben@clab.by>

* Fix & Feat: Assuming and Bounding Fuzz inputs

* Fix linting

* Doc : Fixing by auto-gen doc

* Chore: Removing scratch

* Fix : Moving data length assumption

* Doc: auto-gen doc for invariant

---------
Co-authored-by: clabby <ben@clab.by>

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

 pragma solidity 0.8.15;
 
+import { StdUtils } from "forge-std/Test.sol";
+import { Vm } from "forge-std/Vm.sol";
+
+import { OptimismPortal } from "../../L1/OptimismPortal.sol";
+import { L2OutputOracle } from "../../L1/L2OutputOracle.sol";
+import { AddressAliasHelper } from "../../vendor/AddressAliasHelper.sol";
+import { SystemConfig } from "../../L1/SystemConfig.sol";
+import { ResourceMetering } from "../../L1/ResourceMetering.sol";
+import { Constants } from "../../libraries/Constants.sol";
+
 import { Portal_Initializer } from "../CommonTest.t.sol";
 import { Types } from "../../libraries/Types.sol";
 
+contract OptimismPortal_Depositor is StdUtils, ResourceMetering {
+    Vm internal vm;
+    OptimismPortal internal portal;
+    bool public failedToComplete;
+
+    constructor(Vm _vm, OptimismPortal _portal) {
+        vm = _vm;
+        portal = _portal;
+        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;
+    }
+
+    // A test intended to identify any unexpected halting conditions
+    function depositTransactionCompletes(
+        address _to,
+        uint256 _value,
+        uint64 _gasLimit,
+        bool _isCreation,
+        bytes memory _data
+    ) public payable {
+        vm.assume((!_isCreation || _to == address(0)) && _data.length <= 120_000);
+
+        uint256 preDepositvalue = bound(_value, 0, type(uint128).max);
+        // Give the depositor some ether
+        vm.deal(address(this), preDepositvalue);
+        // cache the contract's eth balance
+        uint256 preDepositBalance = address(this).balance;
+        uint256 value = bound(preDepositvalue, 0, preDepositBalance);
+
+        (, uint64 cachedPrevBoughtGas, ) = ResourceMetering(address(portal)).params();
+        ResourceMetering.ResourceConfig memory rcfg = resourceConfig();
+        uint256 maxResourceLimit = uint64(rcfg.maxResourceLimit);
+        uint64 gasLimit = uint64(
+            bound(
+                _gasLimit,
+                portal.minimumGasLimit(uint64(_data.length)),
+                maxResourceLimit - cachedPrevBoughtGas
+            )
+        );
+
+        try portal.depositTransaction{ value: value }(_to, value, gasLimit, _isCreation, _data) {
+            // Do nothing; Call succeeded
+        } catch {
+            failedToComplete = true;
+        }
+    }
+}
+
 contract OptimismPortal_Invariant_Harness is Portal_Initializer {
     // Reusable default values for a test withdrawal
     Types.WithdrawalTransaction _defaultTx;
@@ -57,6 +132,34 @@ contract OptimismPortal_Invariant_Harness is Portal_Initializer {
     }
 }
 
+contract OptimismPortal_Deposit_Invariant is Portal_Initializer {
+    OptimismPortal_Depositor internal actor;
+
+    function setUp() public override {
+        super.setUp();
+        // Create a deposit actor.
+        actor = new OptimismPortal_Depositor(vm, op);
+
+        targetContract(address(actor));
+
+        bytes4[] memory selectors = new bytes4[](1);
+        selectors[0] = actor.depositTransactionCompletes.selector;
+        FuzzSelector memory selector = FuzzSelector({ addr: address(actor), selectors: selectors });
+        targetSelector(selector);
+    }
+
+    /**
+     * @custom:invariant Deposits of any value should always succeed unless
+     * `_to` = `address(0)` or `_isCreation` = `true`.
+     *
+     * All deposits, barring creation transactions and transactions sent to `address(0)`,
+     * should always succeed.
+     */
+    function invariant_deposit_completes() external {
+        assertEq(actor.failedToComplete(), false);
+    }
+}
+
 contract OptimismPortal_CannotTimeTravel is OptimismPortal_Invariant_Harness {
     function setUp() public override {
         super.setUp();

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

 # `OptimismPortal` Invariants
 
+## Deposits of any value should always succeed unless `_to` = `address(0)` or `_isCreation` = `true`.
+**Test:** [`OptimismPortal.t.sol#L158`](../contracts/test/invariants/OptimismPortal.t.sol#L158)
+
+All deposits, barring creation transactions and transactions sent to `address(0)`, should always succeed. 
+
+
 ## `finalizeWithdrawalTransaction` should revert if the finalization period has not elapsed.
-**Test:** [`OptimismPortal.t.sol#L85`](../contracts/test/invariants/OptimismPortal.t.sol#L85)
+**Test:** [`OptimismPortal.t.sol#L188`](../contracts/test/invariants/OptimismPortal.t.sol#L188)
 
 A withdrawal that has been proven should not be able to be finalized until after the finalization period has elapsed. 
 
 
 ## `finalizeWithdrawalTransaction` should revert if the withdrawal has already been finalized.
-**Test:** [`OptimismPortal.t.sol#L122`](../contracts/test/invariants/OptimismPortal.t.sol#L122)
+**Test:** [`OptimismPortal.t.sol#L225`](../contracts/test/invariants/OptimismPortal.t.sol#L225)
 
 Ensures that there is no chain of calls that can be made that allows a withdrawal to be finalized twice. 
 
 
 ## A withdrawal should **always** be able to be finalized `FINALIZATION_PERIOD_SECONDS` after it was successfully proven.
-**Test:** [`OptimismPortal.t.sol#L157`](../contracts/test/invariants/OptimismPortal.t.sol#L157)
+**Test:** [`OptimismPortal.t.sol#L260`](../contracts/test/invariants/OptimismPortal.t.sol#L260)
 
 This invariant asserts that there is no chain of calls that can be made that will prevent a withdrawal from being finalized exactly `FINALIZATION_PERIOD_SECONDS` after it was successfully proven.