First commit

.gitmodules

@@ -1,3 +1,15 @@
 [submodule "lib/forge-std"]
 	path = lib/forge-std
 	url = https://github.com/foundry-rs/forge-std
+[submodule "lib/halmos-cheatcodes"]
+	path = lib/halmos-cheatcodes
+	url = https://github.com/a16z/halmos-cheatcodes
+[submodule "lib/openzeppelin-contracts"]
+	path = lib/openzeppelin-contracts
+	url = https://github.com/openzeppelin/openzeppelin-contracts
+[submodule "lib/solady"]
+	path = lib/solady
+	url = https://github.com/Vectorized/solady
+[submodule "lib/solmate"]
+	path = lib/solmate
+	url = https://github.com/transmissions11/solmate

remappings.txt

@@ -0,0 +1,4 @@
+@openzeppelin/=lib/openzeppelin-contracts/
+@solady=lib/solady/src
+@solmate=lib/solmate/src
+@src=src

src/ERC20OpenZeppelin.sol

@@ -0,0 +1,23 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.13;
+
+import {ERC20} from "@openzeppelin/contracts/token/ERC20/ERC20.sol";
+
+contract ERC20OpenZeppelin is ERC20 {
+    uint8 private immutable decimals_ = 18;
+
+    constructor(string memory _name, string memory _symbol, uint8 _decimals, address owner, uint256 supply)
+        ERC20(_name, _symbol)
+    {
+        decimals_ = _decimals;
+        _mint(owner, supply);
+    }
+
+    function decimals() public pure override returns (uint8) {
+        return decimals_;
+    }
+
+    function nonces(address) public pure returns (uint256) {
+        return 0;
+    }
+}

src/ERC20Solady.sol

@@ -0,0 +1,42 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.13;
+
+import {ERC20} from "@solady/tokens/ERC20.sol";
+
+contract ERC20Solady is ERC20 {
+    string internal name_;
+    string internal symbol_;
+    uint8 internal decimals_;
+
+    constructor(string memory _name, string memory _symbol, uint8 _decimals, address owner, uint256 supply) {
+        name_ = _name;
+        symbol_ = _symbol;
+        decimals_ = _decimals;
+
+        _mint(owner, supply);
+    }
+
+    function name() public view virtual override returns (string memory) {
+        return name_;
+    }
+
+    function symbol() public view virtual override returns (string memory) {
+        return symbol_;
+    }
+
+    function decimals() public view virtual override returns (uint8) {
+        return decimals_;
+    }
+
+    function nonces(address) public view virtual override returns (uint256) {
+        return 0;
+    }
+
+    function permit(address, address, uint256, uint256, uint8, bytes32, bytes32) public virtual override {
+        revert();
+    }
+
+    function DOMAIN_SEPARATOR() public view virtual override returns (bytes32) {
+        revert();
+    }
+}

src/ERC20Solmate.sol

@@ -0,0 +1,20 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.13;
+
+import {ERC20} from "@solmate/tokens/ERC20.sol";
+
+contract ERC20Solmate is ERC20 {
+    constructor(string memory _name, string memory _symbol, uint8 _decimals, address owner, uint256 supply)
+        ERC20(_name, _symbol, _decimals)
+    {
+        _mint(owner, supply);
+    }
+
+    function permit(address, address, uint256, uint256, uint8, bytes32, bytes32) public virtual override {
+        revert();
+    }
+
+    function DOMAIN_SEPARATOR() public view virtual override returns (bytes32) {
+        revert();
+    }
+}

test/ERC20.t.sol

@@ -0,0 +1,62 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.13;
+
+import {Test} from "forge-std/Test.sol";
+import {SymTest} from "halmos-cheatcodes/SymTest.sol";
+import {ERC20OpenZeppelin} from "@src/ERC20OpenZeppelin.sol";
+import {ERC20Solady} from "@src/ERC20Solady.sol";
+import {ERC20Solmate} from "@src/ERC20Solmate.sol";
+
+contract ERC20Test is Test, SymTest {
+    ERC20OpenZeppelin public openzeppelin;
+    ERC20Solady public solady;
+    ERC20Solmate public solmate;
+
+    function setUp() public {
+        openzeppelin = new ERC20OpenZeppelin("Token", "TOK", 6, msg.sender, 123e18);
+        solady = new ERC20Solady("Token", "TOK", 6, msg.sender, 123e18);
+        solmate = new ERC20Solmate("Token", "TOK", 6, msg.sender, 123e18);
+    }
+
+    function check_differential_staticcall(bytes memory data) public view {
+        address[3] memory contracts = [address(openzeppelin), address(solady), address(solmate)];
+        bool success;
+        bytes memory result;
+        for (uint256 i = 0; i < contracts.length; i++) {
+            (bool _success, bytes memory _result) = contracts[i].staticcall(data);
+            if (i == 0) {
+                success = _success;
+                result = _result;
+            } else {
+                assertEq(success, _success);
+                assertEq(result, _result);
+            }
+        }
+    }
+
+    function check_differential_call(bytes[] memory call, bytes[] memory staticcall) public {
+        address[3] memory contracts = [address(openzeppelin), address(solady), address(solmate)];
+        bool success;
+        bytes memory result;
+        for (uint256 i = 0; i < contracts.length; i++) {
+            (bool _success, bytes memory _result) = contracts[i].call(call[i]);
+            if (i == 0) {
+                success = _success;
+                result = _result;
+            } else {
+                assertEq(success, _success);
+                assertEq(result, _result);
+            }
+        }
+        for (uint256 i = 0; i < staticcall.length; i++) {
+            (bool _success, bytes memory _result) = contracts[i].staticcall(staticcall[i]);
+            if (i == 0) {
+                success = _success;
+                result = _result;
+            } else {
+                assertEq(success, _success);
+                assertEq(result, _result);
+            }
+        }
+    }
+}