feat: external computation diff state wip

packages/contracts-bedrock/.gitignore

@@ -42,3 +42,6 @@ deploy-config/devnetL1.json
 
 # Getting Started guide deploy config
 deploy-config/getting-started.json
+
+# Supererc20 kontrol
+out-kontrol-properties/

packages/contracts-bedrock/foundry.toml

@@ -112,4 +112,10 @@ script = 'test/properties/halmos/'
 src = "test/properties/kontrol"
 test = "test/properties/kontrol"
 script = "test/properties/kontrol"
-out = 'out'
+out = 'out-kontrol-properties'
+# Make sure to export the variables $STATE_DIFF_DIR and $STATE_DIFF_NAME in your shell
+fs_permissions = [
+    { access = 'read', path = './supererc20-state-diff' },
+    { access = 'read-write', path = './supererc20-state-diff/StateDiff.json' },
+    { access = 'read-write', path = './supererc20-state-diff/AddressNames.json' }
+]

packages/contracts-bedrock/supererc20-state-diff/AddressNames.json

@@ -0,0 +1,6 @@
+{
+  "0x2e234DAe75C793f67A35089C9d99245E1C58470b": "sourceToken",
+  "0x5615dEB798BB3E4dFa0139dFa1b3D433Cc23b72f": "superchainERC20Impl",
+  "0x5991A2dF15A8F6A256D3Ec51E99254Cd3fb576A9": "mockL2ToL2Messenger",
+  "0xF62849F9A0B5Bf2913b396098F7c7019b51A820a": "destToken"
+}

packages/contracts-bedrock/test/properties/kontrol/KontrolBase.sol

@@ -0,0 +1,65 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.25;
+
+import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol";
+import { Predeploys } from "src/libraries/Predeploys.sol";
+import { ERC1967Proxy } from "@openzeppelin/contracts-v5/proxy/ERC1967/ERC1967Proxy.sol";
+import { MockL2ToL2Messenger } from "test/properties/halmos/MockL2ToL2Messenger.sol";
+import { KontrolCheats } from "kontrol-cheatcodes/KontrolCheats.sol";
+import { RecordStateDiff } from "./helpers/RecordStateDiff.sol";
+import { Test } from "forge-std/Test.sol";
+
+contract KontrolBase is Test, KontrolCheats, RecordStateDiff {
+    uint256 internal constant CURRENT_CHAIN_ID = 1;
+    uint256 internal constant DESTINATION_CHAIN_ID = 2;
+    uint256 internal constant ZERO_AMOUNT = 0;
+
+    MockL2ToL2Messenger internal constant MESSENGER = MockL2ToL2Messenger(Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER);
+
+    address internal remoteToken = address(bytes20(keccak256("remoteToken")));
+    string internal name = "SuperchainERC20";
+    string internal symbol = "SUPER";
+    uint8 internal decimals = 18;
+
+    OptimismSuperchainERC20 public superchainERC20Impl;
+    OptimismSuperchainERC20 internal sourceToken;
+    OptimismSuperchainERC20 internal destToken;
+    MockL2ToL2Messenger internal mockL2ToL2Messenger;
+
+    // The second function to get the state diff saving the addresses with their names
+    function setUpNamed() public virtual recordStateDiff {
+        // Deploy the OptimismSuperchainERC20 contract implementation and the proxy to be used
+        superchainERC20Impl = new OptimismSuperchainERC20();
+        sourceToken = OptimismSuperchainERC20(
+            address(
+                // TODO: Update to beacon proxy
+                new ERC1967Proxy(
+                    address(superchainERC20Impl),
+                    abi.encodeCall(OptimismSuperchainERC20.initialize, (remoteToken, name, symbol, decimals))
+                )
+            )
+        );
+
+        destToken = OptimismSuperchainERC20(
+            address(
+                // TODO: Update to beacon proxy
+                new ERC1967Proxy(
+                    address(superchainERC20Impl),
+                    abi.encodeCall(OptimismSuperchainERC20.initialize, (remoteToken, name, symbol, decimals))
+                )
+            )
+        );
+
+        mockL2ToL2Messenger =
+            new MockL2ToL2Messenger(address(sourceToken), address(destToken), DESTINATION_CHAIN_ID, address(0));
+
+        save_address(address(superchainERC20Impl), "superchainERC20Impl");
+        save_address(address(sourceToken), "sourceToken");
+        save_address(address(destToken), "destToken");
+        save_address(address(mockL2ToL2Messenger), "mockL2ToL2Messenger");
+    }
+
+    function eqStrings(string memory a, string memory b) internal pure returns (bool) {
+        return keccak256(abi.encode(a)) == keccak256(abi.encode(b));
+    }
+}

packages/contracts-bedrock/test/properties/kontrol/OptimismSuperchain.k.sol → packages/contracts-bedrock/test/properties/kontrol/OptimismSuperchainERC20.k.sol

@@ -3,52 +3,22 @@ pragma solidity 0.8.25;
 
 import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol";
 import { Predeploys } from "src/libraries/Predeploys.sol";
-import { ERC1967Proxy } from "@openzeppelin/contracts-v5/proxy/ERC1967/ERC1967Proxy.sol";
 import { MockL2ToL2Messenger } from "test/properties/halmos/MockL2ToL2Messenger.sol";
-import { HalmosBase } from "test/properties/helpers/HalmosBase.sol";
-import { KontrolCheats } from "kontrol-cheatcodes/KontrolCheats.sol";
-
-contract OptimismSuperchainERC20Kontrol is KontrolCheats, HalmosBase {
-    MockL2ToL2Messenger internal constant MESSENGER = MockL2ToL2Messenger(Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER);
-
-    OptimismSuperchainERC20 public superchainERC20Impl;
-    OptimismSuperchainERC20 internal sourceToken;
-    OptimismSuperchainERC20 internal destToken;
-
-    function setUp() public {
-        // Deploy the OptimismSuperchainERC20 contract implementation and the proxy to be used
-        superchainERC20Impl = new OptimismSuperchainERC20();
-        sourceToken = OptimismSuperchainERC20(
-            address(
-                // TODO: Update to beacon proxy
-                new ERC1967Proxy(
-                    address(superchainERC20Impl),
-                    abi.encodeCall(OptimismSuperchainERC20.initialize, (remoteToken, name, symbol, decimals))
-                )
-            )
-        );
-
-        destToken = OptimismSuperchainERC20(
-            address(
-                // TODO: Update to beacon proxy
-                new ERC1967Proxy(
-                    address(superchainERC20Impl),
-                    abi.encodeCall(OptimismSuperchainERC20.initialize, (remoteToken, name, symbol, decimals))
-                )
-            )
-        );
-
-        // Etch the mocked L2 to L2 Messenger since the messenger logic is out of scope for these test suite. Also, we
-        // avoid issues such as `TSTORE` opcode not being supported, or issues with `encodeVersionedNonce()`
-        address _mockL2ToL2CrossDomainMessenger =
-            address(new MockL2ToL2Messenger(address(sourceToken), address(destToken), DESTINATION_CHAIN_ID, address(0)));
-        vm.etch(address(MESSENGER), _mockL2ToL2CrossDomainMessenger.code);
-        // NOTE: We need to set the crossDomainMessageSender as an immutable or otherwise storage vars and not taken
-        // into account when etching on halmos. Setting a constant slot with setters and getters didn't work neither.
+import { KontrolBase } from "test/properties/kontrol/KontrolBase.sol";
+import { InitialState } from "./deployments/InitialState.sol";
+
+contract OptimismSuperchainERC20Kontrol is KontrolBase, InitialState {
+    function setUpInlined() public {
+        superchainERC20Impl = OptimismSuperchainERC20(superchainERC20ImplAddress);
+        sourceToken = OptimismSuperchainERC20(sourceTokenAddress);
+        destToken = OptimismSuperchainERC20(destTokenAddress);
+        vm.etch(address(MESSENGER), mockL2ToL2MessengerAddress.code);
     }
 
     /// @notice Check setup works as expected
     function prove_setup() public {
+        setUpInlined();
+
         // Source token
         assert(sourceToken.remoteToken() == remoteToken);
         assert(eqStrings(sourceToken.name(), name));
@@ -68,6 +38,8 @@ contract OptimismSuperchainERC20Kontrol is KontrolCheats, HalmosBase {
 
         // Custom cross domain sender
         assert(MESSENGER.crossDomainMessageSender() == address(0));
+
+        assert(block.chainid >= 0);
     }
 
     /// @custom:property-id 6
@@ -81,10 +53,15 @@ contract OptimismSuperchainERC20Kontrol is KontrolCheats, HalmosBase {
     )
         public
     {
+        setUpInlined();
+
         /* Preconditions */
         vm.assume(_to != address(0));
         vm.assume(_from != address(0));
 
+        notBuiltinAddress(_from);
+        notBuiltinAddress(_to);
+
         // Can't deal to unsupported cheatcode
         vm.prank(Predeploys.L2_STANDARD_BRIDGE);
         sourceToken.mint(_from, _initialBalance);
@@ -136,6 +113,9 @@ contract OptimismSuperchainERC20Kontrol is KontrolCheats, HalmosBase {
         vm.assume(_to != address(0));
         vm.assume(_to != address(Predeploys.CROSS_L2_INBOX) && _to != address(MESSENGER));
 
+        notBuiltinAddress(_from);
+        notBuiltinAddress(_to);
+
         uint256 _totalSupplyBefore = sourceToken.totalSupply();
         uint256 _fromBalanceBefore = sourceToken.balanceOf(_from);
         uint256 _toBalanceBefore = sourceToken.balanceOf(_to);

packages/contracts-bedrock/test/properties/kontrol/deployments/InitialState.sol

@@ -0,0 +1,90 @@
+// SPDX-License-Identifier: UNLICENSED
+// This file was autogenerated by running `kontrol load-state`. Do not edit this file manually.
+
+pragma solidity ^0.8.13;
+
+import { Vm } from "forge-std/Vm.sol";
+
+import { InitialStateCode } from "./InitialStateCode.sol";
+
+contract InitialState is InitialStateCode {
+    // Test contract address, 0x7FA9385bE102ac3EAc297483Dd6233D62b3e1496
+    address private constant FOUNDRY_TEST_ADDRESS = 0x7FA9385bE102ac3EAc297483Dd6233D62b3e1496;
+    // Cheat code address, 0x7109709ECfa91a80626fF3989D68f67F5b1DD12D
+    address private constant VM_ADDRESS = address(uint160(uint256(keccak256("hevm cheat code"))));
+    Vm private constant vm = Vm(VM_ADDRESS);
+
+    address internal constant sourceTokenAddress = 0x2e234DAe75C793f67A35089C9d99245E1C58470b;
+    address internal constant superchainERC20ImplAddress = 0x5615dEB798BB3E4dFa0139dFa1b3D433Cc23b72f;
+    address internal constant mockL2ToL2MessengerAddress = 0x5991A2dF15A8F6A256D3Ec51E99254Cd3fb576A9;
+    address internal constant destTokenAddress = 0xF62849F9A0B5Bf2913b396098F7c7019b51A820a;
+
+    function recreateState() public {
+        bytes32 slot;
+        bytes32 value;
+        vm.etch(superchainERC20ImplAddress, superchainERC20ImplCode);
+        slot = hex"f0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00";
+        value = hex"000000000000000000000000000000000000000000000000ffffffffffffffff";
+        vm.store(superchainERC20ImplAddress, slot, value);
+        vm.etch(sourceTokenAddress, sourceTokenCode);
+        slot = hex"360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc";
+        value = hex"0000000000000000000000005615deb798bb3e4dfa0139dfa1b3d433cc23b72f";
+        vm.store(sourceTokenAddress, slot, value);
+        slot = hex"f0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(sourceTokenAddress, slot, value);
+        slot = hex"f0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00";
+        value = hex"0000000000000000000000000000000000000000000000010000000000000001";
+        vm.store(sourceTokenAddress, slot, value);
+        slot = hex"07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb00";
+        value = hex"000000000000000000000000237a66474b7b934b22574359500212977b656d9f";
+        vm.store(sourceTokenAddress, slot, value);
+        slot = hex"07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb01";
+        value = hex"5375706572636861696e4552433230000000000000000000000000000000001e";
+        vm.store(sourceTokenAddress, slot, value);
+        slot = hex"07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb02";
+        value = hex"535550455200000000000000000000000000000000000000000000000000000a";
+        vm.store(sourceTokenAddress, slot, value);
+        slot = hex"07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb03";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000012";
+        vm.store(sourceTokenAddress, slot, value);
+        slot = hex"f0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(sourceTokenAddress, slot, value);
+        vm.etch(destTokenAddress, destTokenCode);
+        slot = hex"360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc";
+        value = hex"0000000000000000000000005615deb798bb3e4dfa0139dfa1b3d433cc23b72f";
+        vm.store(destTokenAddress, slot, value);
+        slot = hex"f0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(destTokenAddress, slot, value);
+        slot = hex"f0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00";
+        value = hex"0000000000000000000000000000000000000000000000010000000000000001";
+        vm.store(destTokenAddress, slot, value);
+        slot = hex"07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb00";
+        value = hex"000000000000000000000000237a66474b7b934b22574359500212977b656d9f";
+        vm.store(destTokenAddress, slot, value);
+        slot = hex"07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb01";
+        value = hex"5375706572636861696e4552433230000000000000000000000000000000001e";
+        vm.store(destTokenAddress, slot, value);
+        slot = hex"07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb02";
+        value = hex"535550455200000000000000000000000000000000000000000000000000000a";
+        vm.store(destTokenAddress, slot, value);
+        slot = hex"07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb03";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000012";
+        vm.store(destTokenAddress, slot, value);
+        slot = hex"f0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(destTokenAddress, slot, value);
+        vm.etch(mockL2ToL2MessengerAddress, mockL2ToL2MessengerCode);
+    }
+
+    function _notExternalAddress(address user) public pure {
+        vm.assume(user != FOUNDRY_TEST_ADDRESS);
+        vm.assume(user != VM_ADDRESS);
+        vm.assume(user != sourceTokenAddress);
+        vm.assume(user != superchainERC20ImplAddress);
+        vm.assume(user != mockL2ToL2MessengerAddress);
+        vm.assume(user != destTokenAddress);
+    }
+}