chore: setup halmos

.gitmodules

@@ -26,3 +26,15 @@
 [submodule "packages/contracts-bedrock/lib/automate"]
 	path = packages/contracts-bedrock/lib/automate
 	url = https://github.com/gelatodigital/automate
+[submodule "packages/contracts-bedrock/lib/halmos-cheatcodes"]
+	path = packages/contracts-bedrock/lib/halmos-cheatcodes
+	url = https://github.com/a16z/halmos-cheatcodes
+[submodule "lib/halmos-cheatcodes"]
+	path = lib/halmos-cheatcodes
+	url = https://github.com/a16z/halmos-cheatcodes
+[submodule "halmos-cheatcodes"]
+	path = halmos-cheatcodes
+	url = https://github.com/a16z/halmos-cheatcodes
+[submodule "packages/contracts-bedrock/halmos-cheatcodes"]
+	path = packages/contracts-bedrock/halmos-cheatcodes
+	url = https://github.com/a16z/halmos-cheatcodes

packages/contracts-bedrock/foundry.toml

@@ -88,3 +88,8 @@ src = 'test/kontrol/proofs'
 out = 'kout-proofs'
 test = 'test/kontrol/proofs'
 script = 'test/kontrol/proofs'
+
+[profile.medusa]
+src = 'test/properties/medusa/'
+test = 'test/properties/medusa/'
+script = 'test/properties/medusa/'

packages/contracts-bedrock/medusa.json

@@ -0,0 +1,82 @@
+{
+	"fuzzing": {
+		"workers": 10,
+		"workerResetLimit": 50,
+		"timeout": 0,
+		"testLimit": 500,
+		"callSequenceLength": 100,
+		"corpusDirectory": "",
+		"coverageEnabled": true,
+		"targetContracts": ["SuperchainERC20FactoryFuzz"],
+		"targetContractsBalances": [],
+		"constructorArgs": {},
+		"deployerAddress": "0x30000",
+		"senderAddresses": [
+			"0x10000",
+			"0x20000",
+			"0x30000"
+		],
+		"blockNumberDelayMax": 60480,
+		"blockTimestampDelayMax": 604800,
+		"blockGasLimit": 125000000,
+		"transactionGasLimit": 12500000,
+		"testing": {
+			"stopOnFailedTest": true,
+			"stopOnFailedContractMatching": false,
+			"stopOnNoTests": true,
+			"testAllContracts": false,
+			"traceAll": false,
+			"assertionTesting": {
+				"enabled": true,
+				"testViewMethods": false,
+				"panicCodeConfig": {
+					"failOnCompilerInsertedPanic": false,
+					"failOnAssertion": true,
+					"failOnArithmeticUnderflow": false,
+					"failOnDivideByZero": false,
+					"failOnEnumTypeConversionOutOfBounds": false,
+					"failOnIncorrectStorageAccess": false,
+					"failOnPopEmptyArray": false,
+					"failOnOutOfBoundsArrayAccess": false,
+					"failOnAllocateTooMuchMemory": false,
+					"failOnCallUninitializedVariable": false
+				}
+			},
+			"propertyTesting": {
+				"enabled": false,
+				"testPrefixes": [
+					"property_"
+				]
+			},
+			"optimizationTesting": {
+				"enabled": false,
+				"testPrefixes": [
+					"optimize_"
+				]
+			},
+			"targetFunctionSignatures": [],
+			"excludeFunctionSignatures": []
+		},
+		"chainConfig": {
+			"codeSizeCheckDisabled": true,
+			"cheatCodes": {
+				"cheatCodesEnabled": true,
+				"enableFFI": false
+			}
+		}
+	},
+	"compilation": {
+		"platform": "crytic-compile",
+		"platformConfig": {
+			"target": ".",
+			"solcVersion": "",
+			"exportDirectory": "",
+			"args": ["--foundry-out-directory", "artifacts","--foundry-compile-all"]
+		}
+	},
+	"logging": {
+		"level": "info",
+		"logDirectory": "",
+		"noColor": false
+	}
+}

packages/contracts-bedrock/package.json

@@ -29,6 +29,7 @@
     "gas-snapshot": "pnpm build:go-ffi && pnpm gas-snapshot:no-build",
     "kontrol-summary": "./test/kontrol/scripts/make-summary-deployment.sh",
     "kontrol-summary-fp": "KONTROL_FP_DEPLOYMENT=true pnpm kontrol-summary",
+    "medusa": "FOUNDRY_PROFILE=medusa medusa fuzz",
     "snapshots": "forge build && npx tsx scripts/autogen/generate-snapshots.ts && pnpm kontrol-summary-fp && pnpm kontrol-summary",
     "snapshots:check": "./scripts/checks/check-snapshots.sh",
     "semver-lock": "forge script scripts/SemverLock.s.sol",
@@ -61,6 +62,7 @@
     "eslint-plugin-jsdoc": "^48.8.3",
     "eslint-plugin-prefer-arrow": "^1.2.3",
     "eslint-plugin-prettier": "^4.0.0",
+    "halmos-cheatcodes": "github:a16z/halmos-cheatcodes#c0d8655",
     "prettier": "^2.8.0",
     "tsx": "^4.16.2",
     "typescript": "^5.5.4"

packages/contracts-bedrock/src/L2/L2StandardBridgeInterop.sol

@@ -0,0 +1,96 @@
+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.15;
+
+import { Predeploys } from "src/libraries/Predeploys.sol";
+import { L2StandardBridge } from "./L2StandardBridge.sol";
+import { IERC20 } from "@openzeppelin/contracts/token/ERC20/IERC20.sol";
+import { IERC20Metadata } from "@openzeppelin/contracts/token/ERC20/extensions/IERC20Metadata.sol";
+
+/// @notice Thrown when the decimals of the tokens are not the same.
+error InvalidDecimals();
+
+/// @notice Thrown when the legacy address is not found in the OptimismMintableERC20Factory.
+error InvalidLegacyAddress();
+
+/// @notice Thrown when the SuperchainERC20 address is not found in the SuperchainERC20Factory.
+error InvalidSuperchainAddress();
+
+/// @notice Thrown when the remote addresses of the tokens are not the same.
+error InvalidTokenPair();
+
+// TODO: Use OptimismMintableERC20Factory contract instead of interface
+interface IOptimismMintableERC20Factory {
+    function deployments(address) external view returns (address);
+}
+
+// TODO: Move to a separate file
+interface ISuperchainERC20Factory {
+    function deployments(address) external view returns (address);
+}
+
+// TODO: Use an existing interface with `mint` and `burn`?
+interface MintableAndBurnable is IERC20 {
+    function mint(address, uint256) external;
+    function burn(address, uint256) external;
+}
+
+/// @custom:proxied
+/// @custom:predeploy 0x4200000000000000000000000000000000000010
+/// @title L2StandardBridgeInterop
+/// @notice The L2StandardBridgeInterop is an extension of the L2StandardBridge that allows for
+///         the conversion of tokens between legacy tokens (OptimismMintableERC20 or StandardL2ERC20)
+///         and SuperchainERC20 tokens.
+contract L2StandardBridgeInterop is L2StandardBridge {
+    /// @notice Emitted when a conversion is made.
+    /// @param from The token being converted from.
+    /// @param to The token being converted to.
+    /// @param caller The caller of the conversion.
+    /// @param amount The amount of tokens being converted.
+    event Converted(address indexed from, address indexed to, address indexed caller, uint256 amount);
+
+    /// @notice Converts `amount` of `from` token to `to` token.
+    /// @param _from The token being converted from.
+    /// @param _to The token being converted to.
+    /// @param _amount The amount of tokens being converted.
+    function convert(address _from, address _to, uint256 _amount) external {
+        _validatePair(_from, _to);
+
+        MintableAndBurnable(_from).burn(msg.sender, _amount);
+        MintableAndBurnable(_to).mint(msg.sender, _amount);
+
+        emit Converted(_from, _to, msg.sender, _amount);
+    }
+
+    /// @notice Validates the pair of tokens.
+    /// @param _from The token being converted from.
+    /// @param _to The token being converted to.
+    function _validatePair(address _from, address _to) internal view {
+        // 1. Decimals check
+        if (IERC20Metadata(_from).decimals() != IERC20Metadata(_to).decimals()) revert InvalidDecimals();
+
+        // Order tokens for factory validation
+        if (_isOptimismMintableERC20(_from)) {
+            _validateFactories(_from, _to);
+        } else {
+            _validateFactories(_to, _from);
+        }
+    }
+
+    /// @notice Validates that the tokens are deployed by the correct factory.
+    /// @param _legacyAddr The legacy token address (OptimismMintableERC20 or StandardL2ERC20).
+    /// @param _superAddr The SuperchainERC20 address.
+    function _validateFactories(address _legacyAddr, address _superAddr) internal view {
+        // 2. Valid legacy check
+        address _legacyRemoteToken =
+            IOptimismMintableERC20Factory(Predeploys.OPTIMISM_MINTABLE_ERC20_FACTORY).deployments(_legacyAddr);
+        if (_legacyRemoteToken == address(0)) revert InvalidLegacyAddress();
+
+        // 3. Valid SuperchainERC20 check
+        address _superRemoteToken =
+            ISuperchainERC20Factory(Predeploys.OPTIMISM_SUPERCHAIN_ERC20_FACTORY).deployments(_superAddr);
+        if (_superRemoteToken == address(0)) revert InvalidSuperchainAddress();
+
+        // 4. Same remote address check
+        if (_legacyRemoteToken != _superRemoteToken) revert InvalidTokenPair();
+    }
+}

packages/contracts-bedrock/src/L2/L2ToL2CrossDomainMessenger.sol

@@ -7,6 +7,7 @@ import { CrossL2Inbox } from "src/L2/CrossL2Inbox.sol";
 import { IL2ToL2CrossDomainMessenger } from "src/L2/IL2ToL2CrossDomainMessenger.sol";
 import { ISemver } from "src/universal/ISemver.sol";
 import { SafeCall } from "src/libraries/SafeCall.sol";
+import "forge-std/Test.sol";
 
 /// @notice Thrown when a non-written slot in transient storage is attempted to be read from.
 error NotEntered();
@@ -123,6 +124,7 @@ contract L2ToL2CrossDomainMessenger is IL2ToL2CrossDomainMessenger, ISemver {
     /// @param _message     Message payload to call target with.
     function sendMessage(uint256 _destination, address _target, bytes calldata _message) external payable {
         if (_destination == block.chainid) revert MessageDestinationSameChain();
+        console.log("block.chainid", block.chainid);
         if (_target == Predeploys.CROSS_L2_INBOX) revert MessageTargetCrossL2Inbox();
         if (_target == Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER) revert MessageTargetL2ToL2CrossDomainMessenger();
 

packages/contracts-bedrock/src/L2/SuperchainERC20.sol

@@ -0,0 +1,140 @@
+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.25;
+
+import { ERC20 } from "@openzeppelin/contracts/token/ERC20/ERC20.sol";
+import { ISuperchainERC20 } from "src/L2/ISuperchainERC20.sol";
+import { IL2ToL2CrossDomainMessenger } from "src/L2/IL2ToL2CrossDomainMessenger.sol";
+import { ISemver } from "src/universal/ISemver.sol";
+import { SafeCall } from "src/libraries/SafeCall.sol";
+import { Predeploys } from "src/libraries/Predeploys.sol";
+
+/// @notice Thrown when attempting to relay a message and the function caller (msg.sender) is not
+/// L2ToL2CrossDomainMessenger.
+error RelayMessageCallerNotL2ToL2CrossDomainMessenger();
+
+/// @notice Thrown when attempting to relay a message and the cross domain message sender is not this SuperchainERC20.
+error MessageSenderNotThisSuperchainERC20();
+
+/// @notice Thrown when attempting to mint or burn tokens and the function caller is not the StandardBridge.
+error CallerNotBridge();
+
+/// @custom:proxied
+/// @title SuperchainERC20
+/// @notice SuperchainERC20 is a standard extension of the base ERC20 token contract that unifies ERC20 token bridging
+///         to make it fungible across the Superchain. This construction builds on top of the L2ToL2CrossDomainMessenger
+///         for both replay protection and domain binding.
+contract SuperchainERC20 is ISuperchainERC20, ERC20, ISemver {
+    /// @notice Address of the L2ToL2CrossDomainMessenger Predeploy.
+    address internal constant MESSENGER = Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER;
+
+    /// @notice Address of the StandardBridge Predeploy.
+    address internal constant BRIDGE = Predeploys.L2_STANDARD_BRIDGE;
+
+    /// @notice Decimals of the token
+    uint8 private immutable DECIMALS;
+
+    /// @notice Address of the corresponding version of this token on the remote chain.
+    address public immutable REMOTE_TOKEN;
+
+    /// @notice Emitted whenever tokens are minted for an account.
+    /// @param account Address of the account tokens are being minted for.
+    /// @param amount  Amount of tokens minted.
+    event Mint(address indexed account, uint256 amount);
+
+    /// @notice Emitted whenever tokens are burned from an account.
+    /// @param account Address of the account tokens are being burned from.
+    /// @param amount  Amount of tokens burned.
+    event Burn(address indexed account, uint256 amount);
+
+    /// @notice Emitted whenever tokens are sent to another chain.
+    /// @param from    Address of the sender.
+    /// @param to      Address of the recipient.
+    /// @param amount  Amount of tokens sent.
+    /// @param chainId Chain ID of the destination chain.
+    event SentERC20(address indexed from, address indexed to, uint256 amount, uint256 chainId);
+
+    /// @notice Emitted whenever tokens are successfully relayed on this chain.
+    /// @param to     Address of the recipient.
+    /// @param amount Amount of tokens relayed.
+    event RelayedERC20(address indexed to, uint256 amount);
+
+    /// @notice A modifier that only allows the bridge to call
+    modifier onlyBridge() {
+        if (msg.sender != BRIDGE) revert CallerNotBridge();
+        _;
+    }
+
+    /// @notice Semantic version.
+    /// @custom:semver 1.0.0
+    string public constant version = "1.0.0";
+
+    /// @param _remoteToken     Address of the corresponding remote token.
+    /// @param _name            ERC20 name.
+    /// @param _symbol          ERC20 symbol.
+    /// @param _decimals        ERC20 decimals.
+    constructor(
+        address _remoteToken,
+        string memory _name,
+        string memory _symbol,
+        uint8 _decimals
+    )
+        ERC20(_name, _symbol)
+    {
+        REMOTE_TOKEN = _remoteToken;
+        DECIMALS = _decimals;
+    }
+
+    /// @notice Allows the StandardBridge to mint tokens.
+    /// @param _to     Address to mint tokens to.
+    /// @param _amount Amount of tokens to mint.
+    function mint(address _to, uint256 _amount) external virtual onlyBridge {
+        _mint(_to, _amount);
+        emit Mint(_to, _amount);
+    }
+
+    /// @notice Allows the StandardBridge to burn tokens.
+    /// @param _from   Address to burn tokens from.
+    /// @param _amount Amount of tokens to burn.
+    function burn(address _from, uint256 _amount) external virtual onlyBridge {
+        _burn(_from, _amount);
+        emit Burn(_from, _amount);
+    }
+
+    /// @notice Sends tokens to some target address on another chain.
+    /// @param _to      Address to send tokens to.
+    /// @param _amount  Amount of tokens to send.
+    /// @param _chainId Chain ID of the destination chain.
+    function sendERC20(address _to, uint256 _amount, uint256 _chainId) external {
+        _burn(msg.sender, _amount);
+
+        bytes memory _message = abi.encodeCall(this.relayERC20, (_to, _amount));
+        IL2ToL2CrossDomainMessenger(MESSENGER).sendMessage(_chainId, address(this), _message);
+
+        emit SentERC20(msg.sender, _to, _amount, _chainId);
+    }
+
+    /// @notice Relays tokens received from another chain.
+    /// @param _to     Address to relay tokens to.
+    /// @param _amount Amount of tokens to relay.
+    function relayERC20(address _to, uint256 _amount) external {
+        if (msg.sender != MESSENGER) revert RelayMessageCallerNotL2ToL2CrossDomainMessenger();
+
+        if (IL2ToL2CrossDomainMessenger(MESSENGER).crossDomainMessageSender() != address(this)) {
+            revert MessageSenderNotThisSuperchainERC20();
+        }
+
+        _mint(_to, _amount);
+
+        emit RelayedERC20(_to, _amount);
+    }
+
+    /// @notice Returns the number of decimals used to get its user representation.
+    /// For example, if `decimals` equals `2`, a balance of `505` tokens should
+    /// be displayed to a user as `5.05` (`505 / 10 ** 2`).
+    /// NOTE: This information is only used for _display_ purposes: it in
+    /// no way affects any of the arithmetic of the contract, including
+    /// {IERC20-balanceOf} and {IERC20-transfer}.
+    function decimals() public view override returns (uint8) {
+        return DECIMALS;
+    }
+}

packages/contracts-bedrock/src/L2/SuperchainERC20Beacon.sol

@@ -0,0 +1,17 @@
+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.25;
+
+import { IBeacon } from "@openzeppelin/contracts/proxy/beacon/IBeacon.sol";
+
+/// @title SuperchainERC20Beacon
+/// @notice SuperchainERC20Beacon is the beacon proxy for the SuperchainERC20 implementation.
+contract SuperchainERC20Beacon is IBeacon {
+    /// TODO: Replace with real implementation address
+    /// @notice Address of the SuperchainERC20 implementation.
+    address internal constant IMPLEMENTATION_ADDRESS = 0x4200000000000000000000000000000000000042;
+
+    /// @inheritdoc IBeacon
+    function implementation() external pure override returns (address) {
+        return IMPLEMENTATION_ADDRESS;
+    }
+}