Merge pull request #5836 from Ratimon/refactor/invariants-encoding

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

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

+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.15;
+
+import { Test } from "forge-std/Test.sol";
+import { StdInvariant } from "forge-std/StdInvariant.sol";
+import { Encoding } from "../../libraries/Encoding.sol";
+
+contract Encoding_Converter {
+    bool public failedRoundtripAToB;
+    bool public failedRoundtripBToA;
+
+    /**
+     * @notice Takes a pair of integers to be encoded into a versioned nonce with the
+     *         Encoding library and then decoded and updates the test contract's state
+     *         indicating if the round trip encoding failed.
+     */
+    function convertRoundTripAToB(uint240 _nonce, uint16 _version) external {
+        // Encode the nonce and version
+        uint256 encodedVersionedNonce = Encoding.encodeVersionedNonce(_nonce, _version);
+
+        // Decode the nonce and version
+        uint240 decodedNonce;
+        uint16 decodedVersion;
+
+        (decodedNonce, decodedVersion) = Encoding.decodeVersionedNonce(encodedVersionedNonce);
+
+        // If our round trip encoding did not return the original result, set our state.
+        if ((decodedNonce != _nonce) || (decodedVersion != _version)) {
+            failedRoundtripAToB = true;
+        }
+    }
+
+    /**
+     * @notice Takes an integer representing a packed version and nonce and attempts
+     *         to decode them using the Encoding library before re-encoding and updates
+     *         the test contract's state indicating if the round trip encoding failed.
+     */
+    function convertRoundTripBToA(uint256 _versionedNonce) external {
+        // Decode the nonce and version
+        uint240 decodedNonce;
+        uint16 decodedVersion;
+
+        (decodedNonce, decodedVersion) = Encoding.decodeVersionedNonce(_versionedNonce);
+
+        // Encode the nonce and version
+        uint256 encodedVersionedNonce = Encoding.encodeVersionedNonce(decodedNonce, decodedVersion);
+
+        // If our round trip encoding did not return the original result, set our state.
+        if (encodedVersionedNonce != _versionedNonce) {
+            failedRoundtripBToA = true;
+        }
+    }
+}
+
+contract Encoding_Invariant is StdInvariant, Test {
+    Encoding_Converter internal actor;
+
+    function setUp() public {
+        // Create a converter actor.
+        actor = new Encoding_Converter();
+
+        targetContract(address(actor));
+
+        bytes4[] memory selectors = new bytes4[](2);
+        selectors[0] = actor.convertRoundTripAToB.selector;
+        selectors[1] = actor.convertRoundTripBToA.selector;
+        FuzzSelector memory selector = FuzzSelector({ addr: address(actor), selectors: selectors });
+        targetSelector(selector);
+    }
+
+    /**
+     * @custom:invariant `convertRoundTripAToB` never fails.
+     *
+     * Asserts that a raw versioned nonce can be encoded / decoded to reach the same raw value.
+     */
+    function invariant_round_trip_encoding_AToB() external {
+        // ASSERTION: The round trip encoding done in testRoundTripAToB(...)
+        assertEq(actor.failedRoundtripAToB(), false);
+    }
+
+    /**
+     * @custom:invariant `convertRoundTripBToA` never fails.
+     *
+     * Asserts that an encoded versioned nonce can always be decoded / re-encoded to reach
+     * the same encoded value.
+     */
+    function invariant_round_trip_encoding_BToA() external {
+        // ASSERTION: The round trip encoding done in testRoundTripBToA should never
+        // fail.
+        assertEq(actor.failedRoundtripBToA(), false);
+    }
+}

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

 # `Encoding` Invariants
 
+## `convertRoundTripAToB` never fails.
+**Test:** [`Encoding.t.sol#L76`](../contracts/test/invariants/Encoding.t.sol#L76)
+
+Asserts that a raw versioned nonce can be encoded / decoded to reach the same raw value. 
+
+
+## `convertRoundTripBToA` never fails.
+**Test:** [`Encoding.t.sol#L87`](../contracts/test/invariants/Encoding.t.sol#L87)
+
+Asserts that an encoded versioned nonce can always be decoded / re-encoded to reach the same encoded value. 
+
+
 ## `testRoundTripAToB` never fails.
 **Test:** [`FuzzEncoding.sol#L56`](../contracts/echidna/FuzzEncoding.sol#L56)