From cf38d27498473cc8375a178b04f1e457fd87645e Mon Sep 17 00:00:00 2001
From: teddy <teddy@defi.sucks>
Date: Thu, 29 Aug 2024 10:35:57 -0300
Subject: [PATCH 01/13] chore: track assertion failures

this is so foundry's invariant contract can check that an assertion
returned false in the handler, while still allowing `fail_on_revert =
false` so we can still take full advantage of medusa's fuzzer & coverage
reports
---
 .../properties/helpers/CompatibleAssert.t.sol | 25 ++++++++++++
 .../medusa/fuzz/Protocol.guided.t.sol         | 39 ++++++++++---------
 .../medusa/fuzz/Protocol.unguided.t.sol       | 25 ++++++------
 .../medusa/properties/Protocol.t.sol          |  8 ++--
 4 files changed, 62 insertions(+), 35 deletions(-)
 create mode 100644 packages/contracts-bedrock/test/properties/helpers/CompatibleAssert.t.sol

diff --git a/packages/contracts-bedrock/test/properties/helpers/CompatibleAssert.t.sol b/packages/contracts-bedrock/test/properties/helpers/CompatibleAssert.t.sol
new file mode 100644
index 000000000000..593e9a9dda20
--- /dev/null
+++ b/packages/contracts-bedrock/test/properties/helpers/CompatibleAssert.t.sol
@@ -0,0 +1,25 @@
+// SPDX-License-Identifier: GPL-3
+pragma solidity ^0.8.24;
+
+import { console } from "forge-std/console.sol";
+
+/// @title CompatibleAssert
+/// @notice meant to add compatibility between medusa assertion tests and
+/// foundry invariant test's required arquitecture
+contract CompatibleAssert {
+    bool public failed;
+
+    function compatibleAssert(bool condition) internal {
+        compatibleAssert(condition, "");
+    }
+
+    function compatibleAssert(bool condition, string memory message) internal {
+        if (!condition) {
+            // for foundry to call & check
+            failed = true;
+            // for medusa
+            console.log("Assertion failed: ", message);
+            assert(false);
+        }
+    }
+}
diff --git a/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.guided.t.sol b/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.guided.t.sol
index d5b5d8b5edc5..e7a37fdc93ca 100644
--- a/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.guided.t.sol
+++ b/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.guided.t.sol
@@ -5,8 +5,9 @@ import { MockL2ToL2CrossDomainMessenger } from "../../helpers/MockL2ToL2CrossDom
 import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol";
 import { ProtocolHandler } from "../handlers/Protocol.t.sol";
 import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol";
+import { CompatibleAssert } from '../../helpers/CompatibleAssert.t.sol';
 
-contract ProtocolGuided is ProtocolHandler {
+contract ProtocolGuided is ProtocolHandler, CompatibleAssert {
     using EnumerableMap for EnumerableMap.Bytes32ToUintMap;
     /// @notice deploy a new supertoken with deploy salt determined by params, to the given (of course mocked) chainId
     /// @custom:property-id 14
@@ -27,7 +28,7 @@ contract ProtocolGuided is ProtocolHandler {
             chainId
         );
         // 14
-        assert(supertoken.totalSupply() == 0);
+        compatibleAssert(supertoken.totalSupply() == 0);
     }
 
     /// @custom:property-id 6
@@ -65,19 +66,19 @@ contract ProtocolGuided is ProtocolHandler {
             uint256 sourceBalanceAfter = sourceToken.balanceOf(currentActor());
             uint256 destinationBalanceAfter = destinationToken.balanceOf(recipient);
             // no free mint
-            assert(sourceBalanceBefore + destinationBalanceBefore == sourceBalanceAfter + destinationBalanceAfter);
+            compatibleAssert(sourceBalanceBefore + destinationBalanceBefore == sourceBalanceAfter + destinationBalanceAfter);
             // 22
-            assert(sourceBalanceBefore - amount == sourceBalanceAfter);
-            assert(destinationBalanceBefore + amount == destinationBalanceAfter);
+            compatibleAssert(sourceBalanceBefore - amount == sourceBalanceAfter);
+            compatibleAssert(destinationBalanceBefore + amount == destinationBalanceAfter);
             uint256 sourceSupplyAfter = sourceToken.totalSupply();
             uint256 destinationSupplyAfter = destinationToken.totalSupply();
             // 23
-            assert(sourceSupplyBefore - amount == sourceSupplyAfter);
-            assert(destinationSupplyBefore + amount == destinationSupplyAfter);
+            compatibleAssert(sourceSupplyBefore - amount == sourceSupplyAfter);
+            compatibleAssert(destinationSupplyBefore + amount == destinationSupplyAfter);
         } catch {
             MESSENGER.setAtomic(false);
             // 6
-            assert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount);
+            compatibleAssert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount);
         }
     }
 
@@ -112,13 +113,13 @@ contract ProtocolGuided is ProtocolHandler {
             ghost_tokensInTransit.set(deploySalt, currentlyInTransit + amount);
             // 26
             uint256 sourceBalanceAfter = sourceToken.balanceOf(currentActor());
-            assert(sourceBalanceBefore - amount == sourceBalanceAfter);
+            compatibleAssert(sourceBalanceBefore - amount == sourceBalanceAfter);
             // 10
             uint256 sourceSupplyAfter = sourceToken.totalSupply();
-            assert(sourceSupplyBefore - amount == sourceSupplyAfter);
+            compatibleAssert(sourceSupplyBefore - amount == sourceSupplyAfter);
         } catch {
             // 6
-            assert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount);
+            compatibleAssert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount);
         }
     }
 
@@ -138,17 +139,17 @@ contract ProtocolGuided is ProtocolHandler {
             bytes32 deploySalt = MESSENGER.superTokenInitDeploySalts(address(destinationToken));
             (bool success, uint256 currentlyInTransit) = ghost_tokensInTransit.tryGet(deploySalt);
             // if sendERC20 didnt intialize this, then test suite is broken
-            assert(success);
+            compatibleAssert(success);
             ghost_tokensInTransit.set(deploySalt, currentlyInTransit - messageToRelay.amount);
             // 11
-            assert(destinationSupplyBefore + messageToRelay.amount == destinationToken.totalSupply());
+            compatibleAssert(destinationSupplyBefore + messageToRelay.amount == destinationToken.totalSupply());
             // 27
-            assert(
+            compatibleAssert(
                 destinationBalanceBefore + messageToRelay.amount == destinationToken.balanceOf(messageToRelay.recipient)
             );
         } catch {
             // 7
-            assert(false);
+            compatibleAssert(false);
         }
     }
 
@@ -194,13 +195,13 @@ contract ProtocolGuided is ProtocolHandler {
             // should not revert because of 7, and if it *does* revert, I want the test suite
             // to discard the sequence instead of potentially getting another
             // error due to the crossDomainMessageSender being manually set
-            assert(false);
+            compatibleAssert(false);
         }
         uint256 balanceSenderAfter = token.balanceOf(currentActor());
         uint256 balanceRecipeintAfter = token.balanceOf(recipient);
         uint256 supplyAfter = token.totalSupply();
-        assert(balanceSenderBefore == balanceSenderAfter);
-        assert(balanceRecipientBefore == balanceRecipeintAfter);
-        assert(supplyBefore == supplyAfter);
+        compatibleAssert(balanceSenderBefore == balanceSenderAfter);
+        compatibleAssert(balanceRecipientBefore == balanceRecipeintAfter);
+        compatibleAssert(supplyBefore == supplyAfter);
     }
 }
diff --git a/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.unguided.t.sol b/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.unguided.t.sol
index 71ba64118088..c3f6d32e79c6 100644
--- a/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.unguided.t.sol
+++ b/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.unguided.t.sol
@@ -4,9 +4,10 @@ pragma solidity ^0.8.25;
 import { ProtocolHandler } from "../handlers/Protocol.t.sol";
 import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol";
 import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol";
+import { CompatibleAssert } from '../../helpers/CompatibleAssert.t.sol';
 
 // TODO: add fuzz_sendERC20 when we implement non-atomic bridging
-contract ProtocolUnguided is ProtocolHandler {
+contract ProtocolUnguided is ProtocolHandler , CompatibleAssert{
     using EnumerableMap for EnumerableMap.Bytes32ToUintMap;
 
     /// @custom:property-id 7
@@ -28,8 +29,8 @@ contract ProtocolUnguided is ProtocolHandler {
         vm.prank(sender);
         try OptimismSuperchainERC20(token).relayERC20(sender, recipient, amount) {
             MESSENGER.setCrossDomainMessageSender(address(0));
-            assert(sender == address(MESSENGER));
-            assert(crossDomainMessageSender == token);
+            compatibleAssert(sender == address(MESSENGER));
+            compatibleAssert(crossDomainMessageSender == token);
             // this increases the supply across chains without a call to
             // `mint` by the MESSENGER, so it kind of breaks an invariant, but
             // let's walk around that:
@@ -37,7 +38,7 @@ contract ProtocolUnguided is ProtocolHandler {
             (, uint256 currentValue) = ghost_totalSupplyAcrossChains.tryGet(salt);
             ghost_totalSupplyAcrossChains.set(salt, currentValue + amount);
         } catch {
-            assert(sender != address(MESSENGER) || crossDomainMessageSender != token);
+            compatibleAssert(sender != address(MESSENGER) || crossDomainMessageSender != token);
             MESSENGER.setCrossDomainMessageSender(address(0));
         }
     }
@@ -71,13 +72,13 @@ contract ProtocolUnguided is ProtocolHandler {
             ghost_tokensInTransit.set(deploySalt, currentlyInTransit + amount);
             // 26
             uint256 sourceBalanceAfter = sourceToken.balanceOf(sender);
-            assert(sourceBalanceBefore - amount == sourceBalanceAfter);
+            compatibleAssert(sourceBalanceBefore - amount == sourceBalanceAfter);
             // 10
             uint256 sourceSupplyAfter = sourceToken.totalSupply();
-            assert(sourceSupplyBefore - amount == sourceSupplyAfter);
+            compatibleAssert(sourceSupplyBefore - amount == sourceSupplyAfter);
         } catch {
             // 6
-            assert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount);
+            compatibleAssert(address(destinationToken) == address(sourceToken) || sourceBalanceBefore < amount);
         }
     }
 
@@ -90,11 +91,11 @@ contract ProtocolUnguided is ProtocolHandler {
         amount = bound(amount, 0, type(uint256).max - OptimismSuperchainERC20(token).totalSupply());
         vm.prank(sender);
         try OptimismSuperchainERC20(token).mint(to, amount) {
-            assert(sender == BRIDGE);
+            compatibleAssert(sender == BRIDGE);
             (, uint256 currentValue) = ghost_totalSupplyAcrossChains.tryGet(salt);
             ghost_totalSupplyAcrossChains.set(salt, currentValue + amount);
         } catch {
-            assert(sender != BRIDGE || to == address(0));
+            compatibleAssert(sender != BRIDGE || to == address(0));
         }
     }
 
@@ -107,11 +108,11 @@ contract ProtocolUnguided is ProtocolHandler {
         uint256 senderBalance = OptimismSuperchainERC20(token).balanceOf(sender);
         vm.prank(sender);
         try OptimismSuperchainERC20(token).burn(from, amount) {
-            assert(sender == BRIDGE);
+            compatibleAssert(sender == BRIDGE);
             (, uint256 currentValue) = ghost_totalSupplyAcrossChains.tryGet(salt);
             ghost_totalSupplyAcrossChains.set(salt, currentValue - amount);
         } catch {
-            assert(sender != BRIDGE || senderBalance < amount);
+            compatibleAssert(sender != BRIDGE || senderBalance < amount);
         }
     }
 
@@ -132,7 +133,7 @@ contract ProtocolUnguided is ProtocolHandler {
         try OptimismSuperchainERC20(allSuperTokens[bound(tokenIndex, 0, allSuperTokens.length)]).initialize(
             remoteToken, name, symbol, decimals
         ) {
-            assert(false);
+            compatibleAssert(false);
         } catch { }
     }
 }
diff --git a/packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol b/packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol
index 7b2f73d54058..2c6e202bd6af 100644
--- a/packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol
+++ b/packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol
@@ -31,7 +31,7 @@ contract ProtocolProperties is ProtocolGuided, ProtocolUnguided, CryticERC20Exte
     /// @custom:property-id 19
     /// @custom:property sum of supertoken total supply across all chains is always <= to convert(legacy, super)-
     /// convert(super, legacy)
-    function property_totalSupplyAcrossChainsEqualsMintsMinusFundsInTransit() external view {
+    function property_totalSupplyAcrossChainsEqualsMintsMinusFundsInTransit() external {
         // iterate over unique deploy salts aka supertokens that are supposed to be compatible with each other
         for (uint256 deploySaltIndex ; deploySaltIndex < ghost_totalSupplyAcrossChains.length(); deploySaltIndex++) {
             uint256 totalSupply ;
@@ -44,7 +44,7 @@ contract ProtocolProperties is ProtocolGuided, ProtocolUnguided, CryticERC20Exte
                     totalSupply += OptimismSuperchainERC20(supertoken).totalSupply();
                 }
             }
-            assert(trackedSupply == totalSupply + fundsInTransit);
+            compatibleAssert(trackedSupply == totalSupply + fundsInTransit);
         }
     }
 
@@ -53,7 +53,7 @@ contract ProtocolProperties is ProtocolGuided, ProtocolUnguided, CryticERC20Exte
     /// @custom:property-id 21
     /// @custom:property sum of supertoken total supply across all chains is equal to convert(legacy, super)-
     /// convert(super, legacy) when all when all cross-chain messages are processed
-    function property_totalSupplyAcrossChainsEqualsMintsWhenQueueIsEmpty() external view {
+    function property_totalSupplyAcrossChainsEqualsMintsWhenQueueIsEmpty() external {
         require(MESSENGER.messageQueueLength() == 0);
         // iterate over unique deploy salts aka supertokens that are supposed to be compatible with each other
         for (uint256 deploySaltIndex ; deploySaltIndex < ghost_totalSupplyAcrossChains.length(); deploySaltIndex++) {
@@ -66,7 +66,7 @@ contract ProtocolProperties is ProtocolGuided, ProtocolUnguided, CryticERC20Exte
                     totalSupply += OptimismSuperchainERC20(supertoken).totalSupply();
                 }
             }
-            assert(trackedSupply == totalSupply);
+            compatibleAssert(trackedSupply == totalSupply);
         }
     }
 }

From e4de5db0583596d7d1d7c09b1912b971a24b7b08 Mon Sep 17 00:00:00 2001
From: teddy <teddy@defi.sucks>
Date: Thu, 29 Aug 2024 20:22:02 -0300
Subject: [PATCH 02/13] fix: explicitly skip duplicate supertoken deployments

---
 .../properties/medusa/handlers/Protocol.t.sol | 24 +++++++++++--------
 1 file changed, 14 insertions(+), 10 deletions(-)

diff --git a/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol b/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol
index 191c5c44a7e6..3f5a3738d5d2 100644
--- a/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol
+++ b/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol
@@ -159,16 +159,20 @@ contract ProtocolHandler is TestBase, StdUtils, Actors {
         // what we use in the tests to walk around two contracts needing two different addresses
         // tbf we could be using CREATE1, but this feels more verbose
         bytes32 hackySalt = keccak256(abi.encode(remoteToken, name, symbol, decimals, chainId));
-        supertoken = OptimismSuperchainERC20(
-            address(
-                // TODO: Use the SuperchainERC20 Beacon Proxy
-                new ERC1967Proxy{ salt: hackySalt }(
-                    address(superchainERC20Impl),
-                    abi.encodeCall(OptimismSuperchainERC20.initialize, (remoteToken, name, symbol, decimals))
-                )
-            )
+        bytes memory creationCode = abi.encode(
+            type(ERC1967Proxy).creationCode,
+            address(superchainERC20Impl),
+            abi.encodeCall(OptimismSuperchainERC20.initialize, (remoteToken, name, symbol, decimals))
         );
-        MESSENGER.registerSupertoken(realSalt, chainId, address(supertoken));
-        allSuperTokens.push(address(supertoken));
+        address ret;
+        assembly ("memory-safe") {
+            ret := create2(0, add(creationCode, 32), mload(creationCode), hackySalt)
+        }
+        if (ret == address(0)) {
+            require(false, "skip duplicate deployment");
+        }
+        MESSENGER.registerSupertoken(realSalt, chainId, ret);
+        allSuperTokens.push(ret);
+        supertoken = OptimismSuperchainERC20(ret);
     }
 }

From 7440c8b25aa769366d48cd133775fc59c0d7a50e Mon Sep 17 00:00:00 2001
From: teddy <teddy@defi.sucks>
Date: Thu, 29 Aug 2024 20:38:17 -0300
Subject: [PATCH 03/13] chore: remove duplicated PROPERTIES.md file

---
 .../test/invariants/PROPERTIES.md             | 73 -------------------
 1 file changed, 73 deletions(-)
 delete mode 100644 packages/contracts-bedrock/test/invariants/PROPERTIES.md

diff --git a/packages/contracts-bedrock/test/invariants/PROPERTIES.md b/packages/contracts-bedrock/test/invariants/PROPERTIES.md
deleted file mode 100644
index 5a5cc71d73b5..000000000000
--- a/packages/contracts-bedrock/test/invariants/PROPERTIES.md
+++ /dev/null
@@ -1,73 +0,0 @@
-# supertoken properties
-
-legend:
-
-- `[ ]`: property not yet tested
-- `**[ ]**`: property not yet tested, dev/research team has asked for extra focus on it
-- `[X]`: tested/proven property
-- `[~]`: partially tested/proven property
-- `:(`: property won't be tested due to some limitation
-
-## Unit test
-
-| id  | description                                                                        | halmos | medusa |
-| --- | ---------------------------------------------------------------------------------- | ------ | ------ |
-| 0   | supertoken token address does not depend on the executing chain’s chainID          | [ ]    | [ ]    |
-| 1   | supertoken token address depends on name, remote token, address and decimals       | [ ]    | [ ]    |
-| 2   | convert() should only allow converting legacy tokens to supertoken and viceversa   | [ ]    | [ ]    |
-| 3   | convert() only allows migrations between tokens representing the same remote asset | [ ]    | [ ]    |
-| 4   | convert() only allows migrations from tokens with the same decimals                | [ ]    | [ ]    |
-| 5   | convert() burns the same amount of one token that it mints of the other            | [ ]    | [ ]    |
-
-## Valid state
-
-| id  | description                                                                                | halmos  | medusa |
-| --- | ------------------------------------------------------------------------------------------ | ------- | ------ |
-| 6   | calls to sendERC20 succeed as long as caller has enough balance                            | [x]     | [ ]    |
-| 7   | calls to relayERC20 always succeed as long as the sender and cross-domain caller are valid | **[~]** | [ ]    |
-
-## Variable transition
-
-| id  | description                                                                                       | halmos | medusa |
-| --- | ------------------------------------------------------------------------------------------------- | ------ | ------ |
-| 8   | sendERC20 with a value of zero does not modify accounting                                         | [x]    | [ ]    |
-| 9   | relayERC20 with a value of zero does not modify accounting                                        | [x]    | [ ]    |
-| 10  | sendERC20 decreases the token's totalSupply in the source chain exactly by the input amount       | [x]    | [ ]    |
-| 11  | relayERC20 increases the token's totalSupply in the destination chain exactly by the input amount | [x]    | [ ]    |
-| 12  | supertoken total supply only increases on calls to mint() by the L2toL2StandardBridge             | [x]    | [ ]    |
-| 13  | supertoken total supply only decreases on calls to burn() by the L2toL2StandardBridge             | [x]    | [ ]    |
-| 14  | supertoken total supply starts at zero                                                            | [x]    | [ ]    |
-| 15  | deploying a supertoken registers its remote token in the factory                                  | [ ]    | [ ]    |
-| 16  | deploying an OptimismMintableERC20 registers its remote token in the factory                      | [ ]    | [ ]    |
-
-## High level
-
-| id  | description                                                                                                                                                           | halmos | medusa |
-| --- | --------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ------ | ------ |
-| 17  | only calls to convert(legacy, super) can increase a supertoken’s total supply across chains                                                                           | [ ]    | [ ]    |
-| 18  | only calls to convert(super, legacy) can decrease a supertoken’s total supply across chains                                                                           | [ ]    | [ ]    |
-| 19  | sum of total supply across all chains is always <= to convert(legacy, super)- convert(super, legacy)                                                                  | [ ]    | [ ]    |
-| 20  | tokens sendERC20-ed on a source chain to a destination chain can be relayERC20-ed on it as long as the source chain is in the dependency set of the destination chain | [ ]    | [ ]    |
-| 21  | sum of supertoken total supply across all chains is = to convert(legacy, super)- convert(super, legacy) when all cross-chain messages are processed                   | [ ]    | [ ]    |
-
-## Atomic bridging pseudo-properties
-
-As another layer of defense, the following properties are defined which assume bridging operations to be atomic (that is, the sequencer and L2Inbox and CrossDomainMessenger contracts are fully abstracted away, `sendERC20` triggering the `relayERC20` call on the same transaction)
-It’s worth noting that these properties will not hold for a live system
-
-| id  | description                                                                                                                        | halmos | medusa |
-| --- | ---------------------------------------------------------------------------------------------------------------------------------- | ------ | ------ |
-| 22  | sendERC20 decreases sender balance in source chain and increases receiver balance in destination chain exactly by the input amount | [ ]    | [x]    |
-| 23  | sendERC20 decreases total supply in source chain and increases it in destination chain exactly by the input amount                 | [ ]    | [x]    |
-| 24  | sum of supertoken total supply across all chains is always equal to convert(legacy, super)- convert(super, legacy)                 | [ ]    | [~]    |
-
-# Expected external interactions
-
-- regular ERC20 operations between any accounts on the same chain, provided by [crytic ERC20 properties](https://github.com/crytic/properties?tab=readme-ov-file#erc20-tests)
-
-# Invariant-breaking candidates (brain dump)
-
-here we’ll list possible interactions that we intend the fuzzing campaign to support in order to help break invariants
-
-- [ ] changing the decimals of tokens after deployment
-- [ ] `convert()` ing between multiple (3+) representations of the same remote token, by having different names/symbols

From dd4388b015f9fb8edb7da345dcecf9e99faadc1e Mon Sep 17 00:00:00 2001
From: teddy <teddy@defi.sucks>
Date: Thu, 29 Aug 2024 21:21:18 -0300
Subject: [PATCH 04/13] chore: expose data to foundry's external invariant
 checker

---
 packages/contracts-bedrock/medusa.json        |  2 +-
 .../properties/helpers/FoundryGetters.t.sol   | 21 +++++++++++++++++++
 .../properties/medusa/handlers/Protocol.t.sol |  2 +-
 3 files changed, 23 insertions(+), 2 deletions(-)
 create mode 100644 packages/contracts-bedrock/test/properties/helpers/FoundryGetters.t.sol

diff --git a/packages/contracts-bedrock/medusa.json b/packages/contracts-bedrock/medusa.json
index 5df25c2cd63b..44e271c4ca34 100644
--- a/packages/contracts-bedrock/medusa.json
+++ b/packages/contracts-bedrock/medusa.json
@@ -28,7 +28,7 @@
 			"traceAll": true,
 			"assertionTesting": {
 				"enabled": true,
-				"testViewMethods": true,
+				"testViewMethods": false,
 				"panicCodeConfig": {
 					"failOnCompilerInsertedPanic": false,
 					"failOnAssertion": true,
diff --git a/packages/contracts-bedrock/test/properties/helpers/FoundryGetters.t.sol b/packages/contracts-bedrock/test/properties/helpers/FoundryGetters.t.sol
new file mode 100644
index 000000000000..8527c0ef180d
--- /dev/null
+++ b/packages/contracts-bedrock/test/properties/helpers/FoundryGetters.t.sol
@@ -0,0 +1,21 @@
+// SPDX-License-Identifier: GPL-3
+pragma solidity ^0.8.24;
+
+import { ProtocolHandler } from "../medusa/handlers/Protocol.t.sol";
+import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol";
+
+contract FoundryGetters is ProtocolHandler {
+    using EnumerableMap for EnumerableMap.Bytes32ToUintMap;
+    function deploySaltsLength() external view returns (uint256 length) {
+        return ghost_totalSupplyAcrossChains.length();
+    }
+
+    function totalSupplyAcrossChainsAtIndex(uint256 index) external view returns (bytes32 salt, uint256 supply) {
+        return ghost_totalSupplyAcrossChains.at(index);
+    }
+
+    function tokensInTransitForDeploySalt(bytes32 salt) external view returns (uint256 amount) {
+        (, amount) = ghost_tokensInTransit.tryGet(salt);
+        return amount;
+    }
+}
diff --git a/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol b/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol
index 3f5a3738d5d2..4e5380126a27 100644
--- a/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol
+++ b/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol
@@ -15,7 +15,7 @@ import { Actors } from "../../helpers/Actors.t.sol";
 contract ProtocolHandler is TestBase, StdUtils, Actors {
     using EnumerableMap for EnumerableMap.Bytes32ToUintMap;
 
-    uint8 internal constant MAX_CHAINS = 4;
+    uint8 public constant MAX_CHAINS = 4;
     uint8 internal constant INITIAL_TOKENS = 1;
     uint8 internal constant INITIAL_SUPERTOKENS = 1;
     uint8 internal constant SUPERTOKEN_INITIAL_MINT = 100;

From 2ec752a1144ca0047e12b3c4c7a8dd62cb1cd04f Mon Sep 17 00:00:00 2001
From: teddy <teddy@defi.sucks>
Date: Thu, 29 Aug 2024 21:23:22 -0300
Subject: [PATCH 05/13] test: run medusa fuzzing campaign from within foundry

---
 .../invariants/OptimismSuperchainERC20.t.sol  | 71 +++++++++++++++++++
 1 file changed, 71 insertions(+)

diff --git a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20.t.sol
index 028a0124e6ca..419625448189 100644
--- a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20.t.sol
+++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20.t.sol
@@ -3,12 +3,83 @@ pragma solidity 0.8.25;
 
 // Testing utilities
 import { Test, StdUtils, Vm } from "forge-std/Test.sol";
+import { StdInvariant } from "forge-std/StdInvariant.sol";
+import { StdAssertions } from "forge-std/StdAssertions.sol";
 import { EIP1967Helper } from "test/mocks/EIP1967Helper.sol";
 
 // Libraries
 import { Predeploys } from "src/libraries/Predeploys.sol";
 import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol";
 import { IL2ToL2CrossDomainMessenger } from "src/L2/IL2ToL2CrossDomainMessenger.sol";
+import { ProtocolGuided } from "../properties/medusa/fuzz/Protocol.guided.t.sol";
+import { ProtocolUnguided } from "../properties/medusa/fuzz/Protocol.unguided.t.sol";
+import { FoundryGetters } from "../properties/helpers/FoundryGetters.t.sol";
+import { MockL2ToL2CrossDomainMessenger } from "../properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol";
+
+contract MedusaCampaignHandler is FoundryGetters, ProtocolGuided, ProtocolUnguided { }
+
+contract OptimismSuperchainERC20MedusaProperties is Test {
+    MedusaCampaignHandler internal handler;
+    MockL2ToL2CrossDomainMessenger internal constant MESSENGER =
+        MockL2ToL2CrossDomainMessenger(Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER);
+
+    function setUp() public {
+        handler = new MedusaCampaignHandler();
+        targetContract(address(handler));
+    }
+
+    // TODO: will need rework after
+    //   - `convert`
+    /// @custom:property-id 19
+    /// @custom:property sum of supertoken total supply across all chains is always <= to convert(legacy, super)-
+    /// convert(super, legacy)
+    function invariant_totalSupplyAcrossChainsEqualsMintsMinusFundsInTransit() external view {
+        // iterate over unique deploy salts aka supertokens that are supposed to be compatible with each other
+        for (uint256 deploySaltIndex = 0; deploySaltIndex < handler.deploySaltsLength(); deploySaltIndex++) {
+            uint256 totalSupply = 0;
+            (bytes32 currentSalt, uint256 trackedSupply) = handler.totalSupplyAcrossChainsAtIndex(deploySaltIndex);
+            uint256 fundsInTransit = handler.tokensInTransitForDeploySalt(currentSalt);
+            // and then over all the (mocked) chain ids where that supertoken could be deployed
+            for (uint256 validChainId = 0; validChainId < handler.MAX_CHAINS(); validChainId++) {
+                address supertoken = MESSENGER.superTokenAddresses(validChainId, currentSalt);
+                if (supertoken != address(0)) {
+                    totalSupply += OptimismSuperchainERC20(supertoken).totalSupply();
+                }
+            }
+            assertEq(trackedSupply, totalSupply + fundsInTransit);
+        }
+    }
+
+    // TODO: will need rework after
+    //   - `convert`
+    /// @custom:property-id 21
+    /// @custom:property sum of supertoken total supply across all chains is equal to convert(legacy, super)-
+    /// convert(super, legacy) when all when all cross-chain messages are processed
+    function invariant_totalSupplyAcrossChainsEqualsMintsWhenQueueIsEmpty() external view {
+        if (MESSENGER.messageQueueLength() != 0) {
+            return;
+        }
+        // iterate over unique deploy salts aka supertokens that are supposed to be compatible with each other
+        for (uint256 deploySaltIndex = 0; deploySaltIndex < handler.deploySaltsLength(); deploySaltIndex++) {
+            uint256 totalSupply = 0;
+            (bytes32 currentSalt, uint256 trackedSupply) = handler.totalSupplyAcrossChainsAtIndex(deploySaltIndex);
+            // and then over all the (mocked) chain ids where that supertoken could be deployed
+            for (uint256 validChainId = 0; validChainId < handler.MAX_CHAINS(); validChainId++) {
+                address supertoken = MESSENGER.superTokenAddresses(validChainId, currentSalt);
+                if (supertoken != address(0)) {
+                    totalSupply += OptimismSuperchainERC20(supertoken).totalSupply();
+                }
+            }
+            assertEq(trackedSupply, totalSupply);
+        }
+    }
+
+    ///@notice `fail_on_revert=false` also ignores StdAssertion failures, so we
+    /// can't simply override compatibleAssert to call StdAssertions.assertTrue
+    function invariant_handlerAssertions() external view {
+        assertFalse(handler.failed());
+    }
+}
 
 /// @title OptimismSuperchainERC20_User
 /// @notice Actor contract that interacts with the OptimismSuperchainERC20 contract.

From a15804c7f569ad9e06329fa1054d4e886f1956a8 Mon Sep 17 00:00:00 2001
From: teddy <teddy@defi.sucks>
Date: Fri, 30 Aug 2024 14:28:30 -0300
Subject: [PATCH 06/13] fix: eagerly check for duplicate deployments

---
 .../properties/medusa/handlers/Protocol.t.sol | 27 +++++++++----------
 1 file changed, 12 insertions(+), 15 deletions(-)

diff --git a/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol b/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol
index 4e5380126a27..c9bc3fd70791 100644
--- a/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol
+++ b/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol
@@ -79,7 +79,6 @@ contract ProtocolHandler is TestBase, StdUtils, Actors {
         index = bound(index, 0, allSuperTokens.length - 1);
         address addr = allSuperTokens[index];
         vm.prank(BRIDGE);
-        // medusa calls with different senders by default
         OptimismSuperchainERC20(addr).mint(currentActor(), amount);
         // currentValue will be zero if key is not present
         (, uint256 currentValue) = ghost_totalSupplyAcrossChains.tryGet(MESSENGER.superTokenInitDeploySalts(addr));
@@ -156,23 +155,21 @@ contract ProtocolHandler is TestBase, StdUtils, Actors {
     {
         // this salt would be used in production. Tokens sharing it will be bridgable with each other
         bytes32 realSalt = keccak256(abi.encode(remoteToken, name, symbol, decimals));
+        require(MESSENGER.superTokenAddresses(chainId, realSalt) == address(0), "skip duplicate deployment");
+
         // what we use in the tests to walk around two contracts needing two different addresses
         // tbf we could be using CREATE1, but this feels more verbose
         bytes32 hackySalt = keccak256(abi.encode(remoteToken, name, symbol, decimals, chainId));
-        bytes memory creationCode = abi.encode(
-            type(ERC1967Proxy).creationCode,
-            address(superchainERC20Impl),
-            abi.encodeCall(OptimismSuperchainERC20.initialize, (remoteToken, name, symbol, decimals))
+        supertoken = OptimismSuperchainERC20(
+            address(
+                // TODO: Use the SuperchainERC20 Beacon Proxy
+                new ERC1967Proxy{ salt: hackySalt }(
+                    address(superchainERC20Impl),
+                    abi.encodeCall(OptimismSuperchainERC20.initialize, (remoteToken, name, symbol, decimals))
+                )
+            )
         );
-        address ret;
-        assembly ("memory-safe") {
-            ret := create2(0, add(creationCode, 32), mload(creationCode), hackySalt)
-        }
-        if (ret == address(0)) {
-            require(false, "skip duplicate deployment");
-        }
-        MESSENGER.registerSupertoken(realSalt, chainId, ret);
-        allSuperTokens.push(ret);
-        supertoken = OptimismSuperchainERC20(ret);
+        MESSENGER.registerSupertoken(realSalt, chainId, address(supertoken));
+        allSuperTokens.push(address(supertoken));
     }
 }

From 63d86dcfb42699f688d1a906fc51201159da80e5 Mon Sep 17 00:00:00 2001
From: teddy <teddy@defi.sucks>
Date: Fri, 30 Aug 2024 14:37:56 -0300
Subject: [PATCH 07/13] fix: feedback from doc

---
 .../test/properties/helpers/CompatibleAssert.t.sol         | 7 +++++--
 .../test/properties/medusa/handlers/Protocol.t.sol         | 2 ++
 2 files changed, 7 insertions(+), 2 deletions(-)

diff --git a/packages/contracts-bedrock/test/properties/helpers/CompatibleAssert.t.sol b/packages/contracts-bedrock/test/properties/helpers/CompatibleAssert.t.sol
index 593e9a9dda20..9cca12bf8649 100644
--- a/packages/contracts-bedrock/test/properties/helpers/CompatibleAssert.t.sol
+++ b/packages/contracts-bedrock/test/properties/helpers/CompatibleAssert.t.sol
@@ -5,7 +5,7 @@ import { console } from "forge-std/console.sol";
 
 /// @title CompatibleAssert
 /// @notice meant to add compatibility between medusa assertion tests and
-/// foundry invariant test's required arquitecture
+/// foundry invariant test's required architecture
 contract CompatibleAssert {
     bool public failed;
 
@@ -15,10 +15,13 @@ contract CompatibleAssert {
 
     function compatibleAssert(bool condition, string memory message) internal {
         if (!condition) {
+            if(bytes(message).length != 0) console.log("Assertion failed: ", message);
+            else console.log("Assertion failed");
+
             // for foundry to call & check
             failed = true;
+
             // for medusa
-            console.log("Assertion failed: ", message);
             assert(false);
         }
     }
diff --git a/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol b/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol
index c9bc3fd70791..bba3f15c5c3a 100644
--- a/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol
+++ b/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol
@@ -155,6 +155,8 @@ contract ProtocolHandler is TestBase, StdUtils, Actors {
     {
         // this salt would be used in production. Tokens sharing it will be bridgable with each other
         bytes32 realSalt = keccak256(abi.encode(remoteToken, name, symbol, decimals));
+        // Foundry invariant erroneously show other unrelated invariant breaking
+        // when this deployment fails due to a create2 collision, so we revert eagerly instead
         require(MESSENGER.superTokenAddresses(chainId, realSalt) == address(0), "skip duplicate deployment");
 
         // what we use in the tests to walk around two contracts needing two different addresses

From 97229c118d26d539d144be00104bbddcc751a59d Mon Sep 17 00:00:00 2001
From: teddy <teddy@defi.sucks>
Date: Mon, 2 Sep 2024 16:37:55 -0300
Subject: [PATCH 08/13] chore: shoehorn medusa campaign into foundry dir
 structure

---
 .gitmodules                                   |   3 -
 packages/contracts-bedrock/foundry.toml       |   6 -
 packages/contracts-bedrock/justfile           |   4 -
 packages/contracts-bedrock/lib/properties     |   1 -
 .../invariants/OptimismSuperchainERC20.t.sol  | 296 ------------------
 .../OptimismSuperchainERC20.t.sol             |  82 +++++
 .../fuzz/Protocol.guided.t.sol                |   4 +-
 .../fuzz/Protocol.unguided.t.sol              |   2 +-
 .../handlers/Protocol.t.sol                   |   6 +-
 .../helpers/Actors.t.sol                      |   0
 .../helpers/CompatibleAssert.t.sol            |   0
 .../helpers/HandlerGetters.t.sol}             |   4 +-
 .../MockL2ToL2CrossDomainMessenger.t.sol      |   0
 ...imismSuperchainERC20ForToBProperties.t.sol |   0
 .../medusa/properties/Protocol.t.sol          |  72 -----
 15 files changed, 90 insertions(+), 390 deletions(-)
 delete mode 160000 packages/contracts-bedrock/lib/properties
 delete mode 100644 packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20.t.sol
 create mode 100644 packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/OptimismSuperchainERC20.t.sol
 rename packages/contracts-bedrock/test/{properties/medusa => invariants/OptimismSuperchainERC20}/fuzz/Protocol.guided.t.sol (98%)
 rename packages/contracts-bedrock/test/{properties/medusa => invariants/OptimismSuperchainERC20}/fuzz/Protocol.unguided.t.sol (98%)
 rename packages/contracts-bedrock/test/{properties/medusa => invariants/OptimismSuperchainERC20}/handlers/Protocol.t.sol (96%)
 rename packages/contracts-bedrock/test/{properties => invariants/OptimismSuperchainERC20}/helpers/Actors.t.sol (100%)
 rename packages/contracts-bedrock/test/{properties => invariants/OptimismSuperchainERC20}/helpers/CompatibleAssert.t.sol (100%)
 rename packages/contracts-bedrock/test/{properties/helpers/FoundryGetters.t.sol => invariants/OptimismSuperchainERC20/helpers/HandlerGetters.t.sol} (86%)
 rename packages/contracts-bedrock/test/{properties => invariants/OptimismSuperchainERC20}/helpers/MockL2ToL2CrossDomainMessenger.t.sol (100%)
 rename packages/contracts-bedrock/test/{properties => invariants/OptimismSuperchainERC20}/helpers/OptimismSuperchainERC20ForToBProperties.t.sol (100%)
 delete mode 100644 packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol

diff --git a/.gitmodules b/.gitmodules
index 7aacfd154993..222d45be7ccc 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -32,6 +32,3 @@
 [submodule "packages/contracts-bedrock/lib/halmos-cheatcodes"]
 	path = packages/contracts-bedrock/lib/halmos-cheatcodes
 	url = https://github.com/a16z/halmos-cheatcodes
-[submodule "packages/contracts-bedrock/lib/properties"]
-	path = packages/contracts-bedrock/lib/properties
-	url = https://github.com/crytic/properties
diff --git a/packages/contracts-bedrock/foundry.toml b/packages/contracts-bedrock/foundry.toml
index 0e0d6959c5b6..4bd9eaff6904 100644
--- a/packages/contracts-bedrock/foundry.toml
+++ b/packages/contracts-bedrock/foundry.toml
@@ -99,12 +99,6 @@ 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/'
-via-ir=true
-
 [profile.halmos]
 src = 'test/properties/halmos/'
 test = 'test/properties/halmos/'
diff --git a/packages/contracts-bedrock/justfile b/packages/contracts-bedrock/justfile
index a003558bb91e..23ea821f30cd 100644
--- a/packages/contracts-bedrock/justfile
+++ b/packages/contracts-bedrock/justfile
@@ -22,10 +22,6 @@ test: build-go-ffi
 test-kontrol:
   ./test/kontrol/scripts/run-kontrol.sh script
 
-test-medusa timeout='100':
-  FOUNDRY_PROFILE=medusa medusa fuzz --timeout {{timeout}}
-
-
 test-halmos-all VERBOSE="-v":
   FOUNDRY_PROFILE=halmos halmos {{VERBOSE}}
 
diff --git a/packages/contracts-bedrock/lib/properties b/packages/contracts-bedrock/lib/properties
deleted file mode 160000
index bb1b78542b3f..000000000000
--- a/packages/contracts-bedrock/lib/properties
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit bb1b78542b3f38e4ae56cf87389cd3ea94387f48
diff --git a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20.t.sol
deleted file mode 100644
index 419625448189..000000000000
--- a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20.t.sol
+++ /dev/null
@@ -1,296 +0,0 @@
-// SPDX-License-Identifier: MIT
-pragma solidity 0.8.25;
-
-// Testing utilities
-import { Test, StdUtils, Vm } from "forge-std/Test.sol";
-import { StdInvariant } from "forge-std/StdInvariant.sol";
-import { StdAssertions } from "forge-std/StdAssertions.sol";
-import { EIP1967Helper } from "test/mocks/EIP1967Helper.sol";
-
-// Libraries
-import { Predeploys } from "src/libraries/Predeploys.sol";
-import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol";
-import { IL2ToL2CrossDomainMessenger } from "src/L2/IL2ToL2CrossDomainMessenger.sol";
-import { ProtocolGuided } from "../properties/medusa/fuzz/Protocol.guided.t.sol";
-import { ProtocolUnguided } from "../properties/medusa/fuzz/Protocol.unguided.t.sol";
-import { FoundryGetters } from "../properties/helpers/FoundryGetters.t.sol";
-import { MockL2ToL2CrossDomainMessenger } from "../properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol";
-
-contract MedusaCampaignHandler is FoundryGetters, ProtocolGuided, ProtocolUnguided { }
-
-contract OptimismSuperchainERC20MedusaProperties is Test {
-    MedusaCampaignHandler internal handler;
-    MockL2ToL2CrossDomainMessenger internal constant MESSENGER =
-        MockL2ToL2CrossDomainMessenger(Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER);
-
-    function setUp() public {
-        handler = new MedusaCampaignHandler();
-        targetContract(address(handler));
-    }
-
-    // TODO: will need rework after
-    //   - `convert`
-    /// @custom:property-id 19
-    /// @custom:property sum of supertoken total supply across all chains is always <= to convert(legacy, super)-
-    /// convert(super, legacy)
-    function invariant_totalSupplyAcrossChainsEqualsMintsMinusFundsInTransit() external view {
-        // iterate over unique deploy salts aka supertokens that are supposed to be compatible with each other
-        for (uint256 deploySaltIndex = 0; deploySaltIndex < handler.deploySaltsLength(); deploySaltIndex++) {
-            uint256 totalSupply = 0;
-            (bytes32 currentSalt, uint256 trackedSupply) = handler.totalSupplyAcrossChainsAtIndex(deploySaltIndex);
-            uint256 fundsInTransit = handler.tokensInTransitForDeploySalt(currentSalt);
-            // and then over all the (mocked) chain ids where that supertoken could be deployed
-            for (uint256 validChainId = 0; validChainId < handler.MAX_CHAINS(); validChainId++) {
-                address supertoken = MESSENGER.superTokenAddresses(validChainId, currentSalt);
-                if (supertoken != address(0)) {
-                    totalSupply += OptimismSuperchainERC20(supertoken).totalSupply();
-                }
-            }
-            assertEq(trackedSupply, totalSupply + fundsInTransit);
-        }
-    }
-
-    // TODO: will need rework after
-    //   - `convert`
-    /// @custom:property-id 21
-    /// @custom:property sum of supertoken total supply across all chains is equal to convert(legacy, super)-
-    /// convert(super, legacy) when all when all cross-chain messages are processed
-    function invariant_totalSupplyAcrossChainsEqualsMintsWhenQueueIsEmpty() external view {
-        if (MESSENGER.messageQueueLength() != 0) {
-            return;
-        }
-        // iterate over unique deploy salts aka supertokens that are supposed to be compatible with each other
-        for (uint256 deploySaltIndex = 0; deploySaltIndex < handler.deploySaltsLength(); deploySaltIndex++) {
-            uint256 totalSupply = 0;
-            (bytes32 currentSalt, uint256 trackedSupply) = handler.totalSupplyAcrossChainsAtIndex(deploySaltIndex);
-            // and then over all the (mocked) chain ids where that supertoken could be deployed
-            for (uint256 validChainId = 0; validChainId < handler.MAX_CHAINS(); validChainId++) {
-                address supertoken = MESSENGER.superTokenAddresses(validChainId, currentSalt);
-                if (supertoken != address(0)) {
-                    totalSupply += OptimismSuperchainERC20(supertoken).totalSupply();
-                }
-            }
-            assertEq(trackedSupply, totalSupply);
-        }
-    }
-
-    ///@notice `fail_on_revert=false` also ignores StdAssertion failures, so we
-    /// can't simply override compatibleAssert to call StdAssertions.assertTrue
-    function invariant_handlerAssertions() external view {
-        assertFalse(handler.failed());
-    }
-}
-
-/// @title OptimismSuperchainERC20_User
-/// @notice Actor contract that interacts with the OptimismSuperchainERC20 contract.
-contract OptimismSuperchainERC20_User is StdUtils {
-    address public immutable receiver;
-
-    /// @notice Cross domain message data.
-    struct MessageData {
-        bytes32 id;
-        uint256 amount;
-    }
-
-    uint256 public totalAmountSent;
-    uint256 public totalAmountRelayed;
-
-    /// @notice Flag to indicate if the test has failed.
-    bool public failed = false;
-
-    /// @notice The Vm contract.
-    Vm internal vm;
-
-    /// @notice The OptimismSuperchainERC20 contract.
-    OptimismSuperchainERC20 internal superchainERC20;
-
-    /// @notice Mapping of sent messages.
-    mapping(bytes32 => bool) internal sent;
-
-    /// @notice Array of unrelayed messages.
-    MessageData[] internal unrelayed;
-
-    /// @param _vm The Vm contract.
-    /// @param _superchainERC20 The OptimismSuperchainERC20 contract.
-    /// @param _balance The initial balance of the contract.
-    constructor(Vm _vm, OptimismSuperchainERC20 _superchainERC20, uint256 _balance, address _receiver) {
-        vm = _vm;
-        superchainERC20 = _superchainERC20;
-
-        // Mint balance to this actor.
-        vm.prank(Predeploys.L2_STANDARD_BRIDGE);
-        superchainERC20.mint(address(this), _balance);
-        receiver = _receiver;
-    }
-
-    /// @notice Send ERC20 tokens to another chain.
-    /// @param _amount The amount of ERC20 tokens to send.
-    /// @param _chainId The chain ID to send the tokens to.
-    /// @param _messageId The message ID.
-    function sendERC20(uint256 _amount, uint256 _chainId, bytes32 _messageId) public {
-        // Make sure we aren't reusing a message ID.
-        if (sent[_messageId]) {
-            return;
-        }
-
-        // Bound send amount to our ERC20 balance.
-        _amount = bound(_amount, 0, superchainERC20.balanceOf(address(this)));
-
-        // Send the amount.
-        try superchainERC20.sendERC20(receiver, _amount, _chainId) {
-            // Success.
-            totalAmountSent += _amount;
-        } catch {
-            failed = true;
-        }
-
-        // Mark message as sent.
-        sent[_messageId] = true;
-        unrelayed.push(MessageData({ id: _messageId, amount: _amount }));
-    }
-
-    /// @notice Relay a message from another chain.
-    function relayMessage(uint256 _source) public {
-        // Make sure there are unrelayed messages.
-        if (unrelayed.length == 0) {
-            return;
-        }
-
-        // Grab the latest unrelayed message.
-        MessageData memory message = unrelayed[unrelayed.length - 1];
-
-        // Simulate the cross-domain message.
-        // Make sure the cross-domain message sender is set to this contract.
-        vm.mockCall(
-            Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER,
-            abi.encodeCall(IL2ToL2CrossDomainMessenger.crossDomainMessageSender, ()),
-            abi.encode(address(superchainERC20))
-        );
-
-        // Simulate the cross-domain message source to any chain.
-        vm.mockCall(
-            Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER,
-            abi.encodeCall(IL2ToL2CrossDomainMessenger.crossDomainMessageSource, ()),
-            abi.encode(_source)
-        );
-
-        // Prank the relayERC20 function.
-        // Balance will just go back to our own account.
-        vm.prank(Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER);
-        try superchainERC20.relayERC20(address(this), receiver, message.amount) {
-            // Success.
-            totalAmountRelayed += message.amount;
-        } catch {
-            failed = true;
-        }
-
-        // Remove the message from the unrelayed list.
-        unrelayed.pop();
-    }
-}
-
-/// @title OptimismSuperchainERC20_Invariant
-/// @notice Invariant test that checks that sending OptimismSuperchainERC20 always succeeds if the actor has a
-///         sufficient balance to do so and that the actor's balance does not increase out of nowhere.
-contract OptimismSuperchainERC20_Invariant is Test {
-    /// @notice Starting balance of the contract.
-    uint256 public constant STARTING_BALANCE = type(uint128).max;
-
-    /// @notice The OptimismSuperchainERC20 contract implementation.
-    address internal optimismSuperchainERC20Impl;
-
-    /// @notice The OptimismSuperchainERC20_User actor.
-    OptimismSuperchainERC20_User internal actor;
-
-    /// @notice The OptimismSuperchainERC20 contract.
-    OptimismSuperchainERC20 internal optimismSuperchainERC20;
-
-    /// @notice The address that will receive the tokens when relaying messages
-    address internal receiver = makeAddr("receiver");
-
-    /// @notice Test setup.
-    function setUp() public {
-        // Deploy the L2ToL2CrossDomainMessenger contract.
-        address _impl = _setImplementationCode(Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER);
-        _setProxyCode(Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER, _impl);
-
-        // Create a new OptimismSuperchainERC20 implementation.
-        optimismSuperchainERC20Impl = address(new OptimismSuperchainERC20());
-
-        // Deploy the OptimismSuperchainERC20 contract.
-        address _proxy = address(0x123456);
-        _setProxyCode(_proxy, optimismSuperchainERC20Impl);
-        optimismSuperchainERC20 = OptimismSuperchainERC20(_proxy);
-
-        // Create a new OptimismSuperchainERC20_User actor.
-        actor = new OptimismSuperchainERC20_User(vm, optimismSuperchainERC20, STARTING_BALANCE, receiver);
-
-        // Set the target contract.
-        targetContract(address(actor));
-
-        // Set the target selectors.
-        bytes4[] memory selectors = new bytes4[](2);
-        selectors[0] = actor.sendERC20.selector;
-        selectors[1] = actor.relayMessage.selector;
-        FuzzSelector memory selector = FuzzSelector({ addr: address(actor), selectors: selectors });
-        targetSelector(selector);
-
-        // Setup assertions
-        assert(optimismSuperchainERC20.balanceOf(address(actor)) == STARTING_BALANCE);
-        assert(optimismSuperchainERC20.balanceOf(address(receiver)) == 0);
-        assert(optimismSuperchainERC20.totalSupply() == STARTING_BALANCE);
-    }
-
-    /// @notice Sets the bytecode in the implementation address.
-    function _setImplementationCode(address _addr) internal returns (address) {
-        string memory cname = Predeploys.getName(_addr);
-        address impl = Predeploys.predeployToCodeNamespace(_addr);
-        vm.etch(impl, vm.getDeployedCode(string.concat(cname, ".sol:", cname)));
-        return impl;
-    }
-
-    /// @notice Sets the bytecode in the proxy address.
-    function _setProxyCode(address _addr, address _impl) internal {
-        bytes memory code = vm.getDeployedCode("universal/Proxy.sol:Proxy");
-        vm.etch(_addr, code);
-        EIP1967Helper.setAdmin(_addr, Predeploys.PROXY_ADMIN);
-        EIP1967Helper.setImplementation(_addr, _impl);
-    }
-
-    /// @notice Invariant that checks that sending OptimismSuperchainERC20 always succeeds.
-    /// @custom:invariant Calls to sendERC20 should always succeed as long as the actor has enough balance.
-    ///                   Actor's balance should also not increase out of nowhere but instead should decrease by the
-    ///                   amount sent.
-    function invariant_sendERC20_succeeds() public view {
-        // Assert that the actor has not failed to send OptimismSuperchainERC20.
-        assertTrue(!actor.failed());
-
-        // Assert that the actor has sent more than or equal to the amount relayed.
-        assertTrue(actor.totalAmountSent() >= actor.totalAmountRelayed());
-
-        // Assert that the actor's balance has decreased by the amount sent.
-        assertEq(optimismSuperchainERC20.balanceOf(address(actor)), STARTING_BALANCE - actor.totalAmountSent());
-
-        // Assert that the total supply of the OptimismSuperchainERC20 contract has decreased by the amount unrelayed.
-        uint256 _unrelayedAmount = actor.totalAmountSent() - actor.totalAmountRelayed();
-        assertEq(optimismSuperchainERC20.totalSupply(), STARTING_BALANCE - _unrelayedAmount);
-    }
-
-    /// @notice Invariant that checks that relaying OptimismSuperchainERC20 always succeeds.
-    /// @custom:invariant Calls to relayERC20 should always succeeds when a message is received from another chain.
-    ///                   Actor's balance should only increase by the amount relayed.
-    function invariant_relayERC20_succeeds() public view {
-        // Assert that the actor has not failed to relay OptimismSuperchainERC20.
-        assertTrue(!actor.failed());
-
-        // Assert that the actor has sent more than or equal to the amount relayed.
-        assertTrue(actor.totalAmountSent() >= actor.totalAmountRelayed());
-
-        // Assert that the actor's balance has increased by the amount relayed.
-        assertEq(optimismSuperchainERC20.balanceOf(address(receiver)), actor.totalAmountRelayed());
-
-        // Assert that the total supply of the OptimismSuperchainERC20 contract has decreased by the amount unrelayed.
-        uint256 _unrelayedAmount = actor.totalAmountSent() - actor.totalAmountRelayed();
-        assertEq(optimismSuperchainERC20.totalSupply(), STARTING_BALANCE - _unrelayedAmount);
-    }
-}
diff --git a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/OptimismSuperchainERC20.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/OptimismSuperchainERC20.t.sol
new file mode 100644
index 000000000000..06d4768ccdb9
--- /dev/null
+++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/OptimismSuperchainERC20.t.sol
@@ -0,0 +1,82 @@
+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.25;
+
+// Testing utilities
+import { Test, StdUtils, Vm } from "forge-std/Test.sol";
+import { StdInvariant } from "forge-std/StdInvariant.sol";
+import { StdAssertions } from "forge-std/StdAssertions.sol";
+import { EIP1967Helper } from "test/mocks/EIP1967Helper.sol";
+
+// Libraries
+import { Predeploys } from "src/libraries/Predeploys.sol";
+import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol";
+import { IL2ToL2CrossDomainMessenger } from "src/L2/IL2ToL2CrossDomainMessenger.sol";
+import { ProtocolGuided } from "./fuzz/Protocol.guided.t.sol";
+import { ProtocolUnguided } from "./fuzz/Protocol.unguided.t.sol";
+import { HandlerGetters } from "./helpers/HandlerGetters.t.sol";
+import { MockL2ToL2CrossDomainMessenger } from "./helpers/MockL2ToL2CrossDomainMessenger.t.sol";
+
+contract OptimismSuperchainERC20Handler is HandlerGetters, ProtocolGuided, ProtocolUnguided { }
+
+contract OptimismSuperchainERC20MedusaProperties is Test {
+    OptimismSuperchainERC20Handler internal handler;
+    MockL2ToL2CrossDomainMessenger internal constant MESSENGER =
+        MockL2ToL2CrossDomainMessenger(Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER);
+
+    function setUp() public {
+        handler = new OptimismSuperchainERC20Handler();
+        targetContract(address(handler));
+    }
+
+    // TODO: will need rework after
+    //   - `convert`
+    /// @custom:property-id 19
+    /// @custom:property sum of supertoken total supply across all chains is always <= to convert(legacy, super)-
+    /// convert(super, legacy)
+    function invariant_totalSupplyAcrossChainsEqualsMintsMinusFundsInTransit() external view {
+        // iterate over unique deploy salts aka supertokens that are supposed to be compatible with each other
+        for (uint256 deploySaltIndex = 0; deploySaltIndex < handler.deploySaltsLength(); deploySaltIndex++) {
+            uint256 totalSupply = 0;
+            (bytes32 currentSalt, uint256 trackedSupply) = handler.totalSupplyAcrossChainsAtIndex(deploySaltIndex);
+            uint256 fundsInTransit = handler.tokensInTransitForDeploySalt(currentSalt);
+            // and then over all the (mocked) chain ids where that supertoken could be deployed
+            for (uint256 validChainId = 0; validChainId < handler.MAX_CHAINS(); validChainId++) {
+                address supertoken = MESSENGER.superTokenAddresses(validChainId, currentSalt);
+                if (supertoken != address(0)) {
+                    totalSupply += OptimismSuperchainERC20(supertoken).totalSupply();
+                }
+            }
+            assertEq(trackedSupply, totalSupply + fundsInTransit);
+        }
+    }
+
+    // TODO: will need rework after
+    //   - `convert`
+    /// @custom:property-id 21
+    /// @custom:property sum of supertoken total supply across all chains is equal to convert(legacy, super)-
+    /// convert(super, legacy) when all when all cross-chain messages are processed
+    function invariant_totalSupplyAcrossChainsEqualsMintsWhenQueueIsEmpty() external view {
+        if (MESSENGER.messageQueueLength() != 0) {
+            return;
+        }
+        // iterate over unique deploy salts aka supertokens that are supposed to be compatible with each other
+        for (uint256 deploySaltIndex = 0; deploySaltIndex < handler.deploySaltsLength(); deploySaltIndex++) {
+            uint256 totalSupply = 0;
+            (bytes32 currentSalt, uint256 trackedSupply) = handler.totalSupplyAcrossChainsAtIndex(deploySaltIndex);
+            // and then over all the (mocked) chain ids where that supertoken could be deployed
+            for (uint256 validChainId = 0; validChainId < handler.MAX_CHAINS(); validChainId++) {
+                address supertoken = MESSENGER.superTokenAddresses(validChainId, currentSalt);
+                if (supertoken != address(0)) {
+                    totalSupply += OptimismSuperchainERC20(supertoken).totalSupply();
+                }
+            }
+            assertEq(trackedSupply, totalSupply);
+        }
+    }
+
+    ///@notice `fail_on_revert=false` also ignores StdAssertion failures, so we
+    /// can't simply override compatibleAssert to call StdAssertions.assertTrue
+    function invariant_handlerAssertions() external view {
+        assertFalse(handler.failed());
+    }
+}
diff --git a/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.guided.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/fuzz/Protocol.guided.t.sol
similarity index 98%
rename from packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.guided.t.sol
rename to packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/fuzz/Protocol.guided.t.sol
index e7a37fdc93ca..2d9c8d52fab3 100644
--- a/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.guided.t.sol
+++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/fuzz/Protocol.guided.t.sol
@@ -1,11 +1,11 @@
 // SPDX-License-Identifier: MIT
 pragma solidity ^0.8.25;
 
-import { MockL2ToL2CrossDomainMessenger } from "../../helpers/MockL2ToL2CrossDomainMessenger.t.sol";
+import { MockL2ToL2CrossDomainMessenger } from "../helpers/MockL2ToL2CrossDomainMessenger.t.sol";
 import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol";
 import { ProtocolHandler } from "../handlers/Protocol.t.sol";
 import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol";
-import { CompatibleAssert } from '../../helpers/CompatibleAssert.t.sol';
+import { CompatibleAssert } from '../helpers/CompatibleAssert.t.sol';
 
 contract ProtocolGuided is ProtocolHandler, CompatibleAssert {
     using EnumerableMap for EnumerableMap.Bytes32ToUintMap;
diff --git a/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.unguided.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/fuzz/Protocol.unguided.t.sol
similarity index 98%
rename from packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.unguided.t.sol
rename to packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/fuzz/Protocol.unguided.t.sol
index c3f6d32e79c6..bf6d1386d409 100644
--- a/packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.unguided.t.sol
+++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/fuzz/Protocol.unguided.t.sol
@@ -4,7 +4,7 @@ pragma solidity ^0.8.25;
 import { ProtocolHandler } from "../handlers/Protocol.t.sol";
 import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol";
 import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol";
-import { CompatibleAssert } from '../../helpers/CompatibleAssert.t.sol';
+import { CompatibleAssert } from '../helpers/CompatibleAssert.t.sol';
 
 // TODO: add fuzz_sendERC20 when we implement non-atomic bridging
 contract ProtocolUnguided is ProtocolHandler , CompatibleAssert{
diff --git a/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/handlers/Protocol.t.sol
similarity index 96%
rename from packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol
rename to packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/handlers/Protocol.t.sol
index bba3f15c5c3a..921495b467ab 100644
--- a/packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.t.sol
+++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/handlers/Protocol.t.sol
@@ -7,10 +7,10 @@ import { StdUtils } from "forge-std/StdUtils.sol";
 import { ERC1967Proxy } from "@openzeppelin/contracts-v5/proxy/ERC1967/ERC1967Proxy.sol";
 import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol";
 import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol";
-import { OptimismSuperchainERC20ForToBProperties } from "../../helpers/OptimismSuperchainERC20ForToBProperties.t.sol";
+import { OptimismSuperchainERC20ForToBProperties } from "../helpers/OptimismSuperchainERC20ForToBProperties.t.sol";
 import { Predeploys } from "src/libraries/Predeploys.sol";
-import { MockL2ToL2CrossDomainMessenger } from "../../helpers/MockL2ToL2CrossDomainMessenger.t.sol";
-import { Actors } from "../../helpers/Actors.t.sol";
+import { MockL2ToL2CrossDomainMessenger } from "../helpers/MockL2ToL2CrossDomainMessenger.t.sol";
+import { Actors } from "../helpers/Actors.t.sol";
 
 contract ProtocolHandler is TestBase, StdUtils, Actors {
     using EnumerableMap for EnumerableMap.Bytes32ToUintMap;
diff --git a/packages/contracts-bedrock/test/properties/helpers/Actors.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/Actors.t.sol
similarity index 100%
rename from packages/contracts-bedrock/test/properties/helpers/Actors.t.sol
rename to packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/Actors.t.sol
diff --git a/packages/contracts-bedrock/test/properties/helpers/CompatibleAssert.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/CompatibleAssert.t.sol
similarity index 100%
rename from packages/contracts-bedrock/test/properties/helpers/CompatibleAssert.t.sol
rename to packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/CompatibleAssert.t.sol
diff --git a/packages/contracts-bedrock/test/properties/helpers/FoundryGetters.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/HandlerGetters.t.sol
similarity index 86%
rename from packages/contracts-bedrock/test/properties/helpers/FoundryGetters.t.sol
rename to packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/HandlerGetters.t.sol
index 8527c0ef180d..6120f5f75684 100644
--- a/packages/contracts-bedrock/test/properties/helpers/FoundryGetters.t.sol
+++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/HandlerGetters.t.sol
@@ -1,10 +1,10 @@
 // SPDX-License-Identifier: GPL-3
 pragma solidity ^0.8.24;
 
-import { ProtocolHandler } from "../medusa/handlers/Protocol.t.sol";
+import { ProtocolHandler } from "../handlers/Protocol.t.sol";
 import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol";
 
-contract FoundryGetters is ProtocolHandler {
+contract HandlerGetters is ProtocolHandler {
     using EnumerableMap for EnumerableMap.Bytes32ToUintMap;
     function deploySaltsLength() external view returns (uint256 length) {
         return ghost_totalSupplyAcrossChains.length();
diff --git a/packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/MockL2ToL2CrossDomainMessenger.t.sol
similarity index 100%
rename from packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol
rename to packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/MockL2ToL2CrossDomainMessenger.t.sol
diff --git a/packages/contracts-bedrock/test/properties/helpers/OptimismSuperchainERC20ForToBProperties.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/OptimismSuperchainERC20ForToBProperties.t.sol
similarity index 100%
rename from packages/contracts-bedrock/test/properties/helpers/OptimismSuperchainERC20ForToBProperties.t.sol
rename to packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/helpers/OptimismSuperchainERC20ForToBProperties.t.sol
diff --git a/packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol b/packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol
deleted file mode 100644
index 2c6e202bd6af..000000000000
--- a/packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol
+++ /dev/null
@@ -1,72 +0,0 @@
-// SPDX-License-Identifier: MIT
-pragma solidity ^0.8.25;
-
-import { ITokenMock } from "@crytic/properties/contracts/ERC20/external/util/ITokenMock.sol";
-import { EnumerableMap } from "@openzeppelin/contracts/utils/structs/EnumerableMap.sol";
-import { ProtocolGuided } from "../fuzz/Protocol.guided.t.sol";
-import { ProtocolUnguided } from "../fuzz/Protocol.unguided.t.sol";
-import { CryticERC20ExternalBasicProperties } from
-    "@crytic/properties/contracts/ERC20/external/properties/ERC20ExternalBasicProperties.sol";
-import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol";
-
-contract ProtocolProperties is ProtocolGuided, ProtocolUnguided, CryticERC20ExternalBasicProperties {
-    using EnumerableMap for EnumerableMap.Bytes32ToUintMap;
-
-    /// @dev `token` is the token under test for the ToB properties. This is coupled
-    /// to the ProtocolSetup constructor initializing at least one supertoken
-    constructor() {
-        token = ITokenMock(allSuperTokens[0]);
-    }
-
-    /// @dev not that much of a handler, since this only changes which
-    /// supertoken the ToB assertions are performed against. Thankfully, they are
-    /// implemented in a way that don't require tracking ghost variables or can
-    /// break properties defined by us
-    function handler_ToBTestOtherToken(uint256 index) external {
-        token = ITokenMock(allSuperTokens[bound(index, 0, allSuperTokens.length - 1)]);
-    }
-
-    // TODO: will need rework after
-    //   - `convert`
-    /// @custom:property-id 19
-    /// @custom:property sum of supertoken total supply across all chains is always <= to convert(legacy, super)-
-    /// convert(super, legacy)
-    function property_totalSupplyAcrossChainsEqualsMintsMinusFundsInTransit() external {
-        // iterate over unique deploy salts aka supertokens that are supposed to be compatible with each other
-        for (uint256 deploySaltIndex ; deploySaltIndex < ghost_totalSupplyAcrossChains.length(); deploySaltIndex++) {
-            uint256 totalSupply ;
-            (bytes32 currentSalt, uint256 trackedSupply) = ghost_totalSupplyAcrossChains.at(deploySaltIndex);
-            (, uint256 fundsInTransit) = ghost_tokensInTransit.tryGet(currentSalt);
-            // and then over all the (mocked) chain ids where that supertoken could be deployed
-            for (uint256 validChainId ; validChainId < MAX_CHAINS; validChainId++) {
-                address supertoken = MESSENGER.superTokenAddresses(validChainId, currentSalt);
-                if (supertoken != address(0)) {
-                    totalSupply += OptimismSuperchainERC20(supertoken).totalSupply();
-                }
-            }
-            compatibleAssert(trackedSupply == totalSupply + fundsInTransit);
-        }
-    }
-
-    // TODO: will need rework after
-    //   - `convert`
-    /// @custom:property-id 21
-    /// @custom:property sum of supertoken total supply across all chains is equal to convert(legacy, super)-
-    /// convert(super, legacy) when all when all cross-chain messages are processed
-    function property_totalSupplyAcrossChainsEqualsMintsWhenQueueIsEmpty() external {
-        require(MESSENGER.messageQueueLength() == 0);
-        // iterate over unique deploy salts aka supertokens that are supposed to be compatible with each other
-        for (uint256 deploySaltIndex ; deploySaltIndex < ghost_totalSupplyAcrossChains.length(); deploySaltIndex++) {
-            uint256 totalSupply ;
-            (bytes32 currentSalt, uint256 trackedSupply) = ghost_totalSupplyAcrossChains.at(deploySaltIndex);
-            // and then over all the (mocked) chain ids where that supertoken could be deployed
-            for (uint256 validChainId ; validChainId < MAX_CHAINS; validChainId++) {
-                address supertoken = MESSENGER.superTokenAddresses(validChainId, currentSalt);
-                if (supertoken != address(0)) {
-                    totalSupply += OptimismSuperchainERC20(supertoken).totalSupply();
-                }
-            }
-            compatibleAssert(trackedSupply == totalSupply);
-        }
-    }
-}

From 5a82573a35f79b3df79c82a41a723f5905c6afbf Mon Sep 17 00:00:00 2001
From: teddy <teddy@defi.sucks>
Date: Mon, 2 Sep 2024 16:49:14 -0300
Subject: [PATCH 09/13] chore: remove PROPERTIES.md file

---
 .../test/properties/PROPERTIES.md             | 141 ------------------
 1 file changed, 141 deletions(-)
 delete mode 100644 packages/contracts-bedrock/test/properties/PROPERTIES.md

diff --git a/packages/contracts-bedrock/test/properties/PROPERTIES.md b/packages/contracts-bedrock/test/properties/PROPERTIES.md
deleted file mode 100644
index d915d565633e..000000000000
--- a/packages/contracts-bedrock/test/properties/PROPERTIES.md
+++ /dev/null
@@ -1,141 +0,0 @@
-# Supertoken advanced testing
-
-## Overview
-
-This document defines a set of properties global to the supertoken ecosystem, for which we will:
-
-- run a [Medusa](https://github.com/crytic/medusa) fuzzing campaign, trying to break system invariants
-- formally prove with [Halmos](https://github.com/a16z/halmos) whenever possible
-
-## Milestones
-
-The supertoken ecosystem consists of not just the supertoken contract, but the required changes to other contracts for liquidity to reach the former.
-
-Considering only the supertoken contract is merged into the `develop` branch, and work for the other components is still in progress, we define three milestones for the testing campaign:
-
-- SupERC20: concerned with only the supertoken contract, the first one to be implemented
-- Factories: covers the above + the development of `OptimismSuperchainERC20Factory` and required changes to `OptimismMintableERC20Factory`
-- Liquidity Migration: includes the `convert` function on the `L2StandardBridgeInterop` to migrate liquidity from legacy tokens into supertokens
-
-## Where to place the testing campaign
-
-Given the [OP monorepo](https://github.com/ethereum-optimism/optimism) already has invariant testing provided by foundry, it's not a trivial matter where to place this advanced testing campaign. Two alternatives are proposed:
-
-- including it in the mainline OP monorepo, in a subdirectory of the existing test contracts such as `test/invariants/medusa/superc20/`
-- keep the campaign in wonderland's fork of the repository, in its own feature branch, in which case the deliverable would consist primarily of:
-    - a summary of the results, extending this document
-    - PRs with extra unit tests replicating found issues to the main repo where applicable
-
-## Contracts in scope
-
-- [ ]  [OptimismMintableERC20Factory](https://github.com/defi-wonderland/optimism/blob/develop/packages/contracts-bedrock/src/universal/OptimismMintableERC20Factory.sol) (modifications to enable `convert` not yet merged)
-- [ ]  [OptimismSuperchainERC20](https://github.com/defi-wonderland/optimism/blob/develop/packages/contracts-bedrock/src/L2/OptimismSuperchainERC20.sol1)
-- [ ]  [OptimismSuperchainERC20Factory](https://github.com/defi-wonderland/optimism/pull/8/files#diff-09838f5703c353d0f7c5ff395acc04c1768ef58becac67404bc17e1fb0018517) (not yet merged)
-- [ ]  [L2StandardBridgeInterop](https://github.com/defi-wonderland/optimism/pull/10/files#diff-56cf869412631eac0a04a03f7d026596f64a1e00fcffa713bc770d67c6856c2f) (not yet merged)
-
-## Behavior assumed correct
-
-- [ ]  inclusion of relay transactions
-- [ ]  sequencer implementation
-- [ ]  [OptimismMintableERC20](https://github.com/defi-wonderland/optimism/blob/develop/packages/contracts-bedrock/src/universal/OptimismMintableERC20.sol)
-- [ ]  [L2ToL2CrossDomainMessenger](https://github.com/defi-wonderland/optimism/blob/develop/packages/contracts-bedrock/src/L2/L2CrossDomainMessenger.sol)
-- [ ]  [CrossL2Inbox](https://github.com/defi-wonderland/src/L2/CrossL2Inbox.sol)
-
-## Pain points
-
-- existing fuzzing tools use the same EVM to run the tested contracts as they do for asserting invariants, tracking ghost variables and everything else necessary to provision a fuzzing campaign. While this is usually very convenient, it means that we can’t assert on the behaviour/state of *different* chains from within a fuzzing campaign. This means we will have to walk around the requirement of supertokens having the same address across all chains, and implement a way to mock tokens existing in different chains. We will strive to formally prove it in a unitary fashion to mitigate this in properties 0 and 1
-- a buffer to represent 'in transit' messages should be implemented to assert on invariants relating to the non-atomicity of bridging from one chain to another. It is yet to be determined if it’ll be a FIFO queue (assuming ideal message ordering by sequencers) or it’ll have random-access capability to simulate messages arriving out of order
-
-## Definitions
-
-- *legacy token:*  an OptimismMintableERC20 or L2StandardERC20 token on the suprechain that has either been deployed by the factory after the liquidity migration upgrade to the latter, or has been deployed before it **but** added to factory’s `deployments` mapping as part of the upgrade. This testing campaign is not concerned with tokens on L1 or not listed in the factory’s `deployments` mapping.
-- *supertoken:* a SuperchainERC20 contract deployed by the `OptimismSuperchainERC20Factory`
-
-# Ecosystem properties
-
-legend:
-
-- `[ ]`: property not yet tested
-- `**[ ]**`: property not yet tested, dev/research team has asked for extra focus on it
-- `[X]`: tested/proven property
-- `[~]`: partially tested/proven property
-- `:(`: property won't be tested due to some limitation
-
-## Unit test
-
-| id  | milestone           | description                                                                                | halmos | medusa |
-| --- | ---                 | ---                                                                                        | ---    | ---    |
-| 0   | Factories           | supertoken token address does not depend on the executing chain’s chainID                  | [ ]    | [ ]    |
-| 1   | Factories           | supertoken token address depends on remote token, name, symbol and decimals                | [ ]    | [ ]    |
-| 2   | Liquidity Migration | convert() should only allow converting legacy tokens to supertoken and viceversa           | [ ]    | [ ]    |
-| 3   | Liquidity Migration | convert() only allows migrations between tokens representing the same remote asset         | [ ]    | [ ]    |
-| 4   | Liquidity Migration | convert() only allows migrations from tokens with the same decimals                        | [ ]    | [ ]    |
-| 5   | Liquidity Migration | convert() burns the same amount of legacy token that it mints of supertoken, and viceversa | [ ]    | [ ]    |
-| 25  | SupERC20            | supertokens can't be reinitialized                                                         | [ ]    | [x]    |
-
-## Valid state
-
-| id  | milestone | description                                                                    | halmos  | medusa |
-| --- | ---       | ---                                                                            | ---     | ---    |
-| 6   | SupERC20  | calls to sendERC20 succeed as long as caller has enough balance                | [x]     | [x]    |
-| 7   | SupERC20  | calls to relayERC20 always succeed as long as the cross-domain caller is valid | **[~]** | [~]    |
-
-## Variable transition
-
-| id  | milestone           | description                                                                                       | halmos | medusa |
-| --- | ---                 | ---                                                                                               | ---    | ---    |
-| 8   | SupERC20            | sendERC20 with a value of zero does not modify accounting                                         | [x]    | [x]    |
-| 9   | SupERC20            | relayERC20 with a value of zero does not modify accounting                                        | [x]    | [x]    |
-| 10  | SupERC20            | sendERC20 decreases the token's totalSupply in the source chain exactly by the input amount       | [x]    | [x]    |
-| 26  | SupERC20            | sendERC20 decreases the sender's balance in the source chain exactly by the input amount          | [ ]    | [x]    |
-| 27  | SupERC20            | relayERC20 increases sender's balance in the destination chain exactly by the input amount        | [ ]    | [x]    |
-| 11  | SupERC20            | relayERC20 increases the token's totalSupply in the destination chain exactly by the input amount | [x]    | [ ]    |
-| 12  | Liquidity Migration | supertoken total supply only increases on calls to mint() by the L2toL2StandardBridge             | [x]    | [~]    |
-| 13  | Liquidity Migration | supertoken total supply only decreases on calls to burn() by the L2toL2StandardBridge             | [x]    | [ ]    |
-| 14  | SupERC20            | supertoken total supply starts at zero                                                            | [x]    | [x]    |
-| 15  | Factories           | deploying a supertoken registers its remote token in the factory                                  | [ ]    | [ ]    |
-| 16  | Factories           | deploying an OptimismMintableERC20 registers its remote token in the factory                      | [ ]    | [ ]    |
-
-## High level
-
-| id  | milestone           | description                                                                                                                                                           | halmos | medusa |
-| --- | ---                 | ---                                                                                                                                                                   | ---    | ---    |
-| 17  | Liquidity Migration | only calls to convert(legacy, super) can increase a supertoken’s  total supply across chains                                                                          | [ ]    | [ ]    |
-| 18  | Liquidity Migration | only calls to convert(super, legacy) can decrease a supertoken’s  total supply across chains                                                                          | [ ]    | [ ]    |
-| 19  | Liquidity Migration | sum of supertoken total supply across all chains is always <= to convert(legacy, super)- convert(super, legacy)                                                       | [ ]    | [~]    |
-| 20  | SupERC20            | tokens sendERC20-ed on a source chain to a destination chain can be relayERC20-ed on it as long as the source chain is in the dependency set of the destination chain | [ ]    | [ ]    |
-| 21  | Liquidity Migration | sum of supertoken total supply across all chains is = to convert(legacy, super)- convert(super, legacy) when all cross-chain messages are processed                   | [ ]    | [~]    |
-
-## Atomic bridging pseudo-properties
-
-As another layer of defense, the following properties are defined which assume bridging operations to be atomic (that is, the sequencer and L2Inbox and CrossDomainMessenger contracts are fully abstracted away, `sendERC20` triggering the `relayERC20` call on the same transaction)
-It’s worth noting that these properties will not hold for a live system
-
-| id  | milestone           | description                                                                                                                        | halmos | medusa |
-| --- | ---                 | ---                                                                                                                                | ---    | ---    |
-| 22  | SupERC20            | sendERC20 decreases sender balance in source chain and increases receiver balance in destination chain exactly by the input amount | [ ]    | [x]    |
-| 23  | SupERC20            | sendERC20 decreases total supply in source chain and increases it in destination chain exactly by the input amount                 | [ ]    | [x]    |
-| 24  | Liquidity Migration | sum of supertoken total supply across all chains is always equal to convert(legacy, super)- convert(super, legacy)                 | [ ]    | [~]    |
-
-# Expected external interactions
-
-- [x] regular ERC20 operations between any accounts on the same chain, provided by [crytic ERC20 properties](https://github.com/crytic/properties?tab=readme-ov-file#erc20-tests)
-
-# Invariant-breaking candidates (brain dump)
-
-here we’ll list possible interactions that we intend the fuzzing campaign to support in order to help break invariants
-
-- [ ]  changing the decimals of tokens after deployment
-- [ ]  `convert()` ing between multiple (3+) representations of the same remote token, by having different names/symbols
-
-# Internal structure
-
-## Medusa campaign
-
-Fuzzing campaigns have both the need to push the contract into different states (state transitions) and assert properties are actually held. This defines a spectrum of function types:
-
-- `handler_`: they only transition the protocol state, and don't perform any assertions.
-- `fuzz_`: they both transition the protocol state and perform assertions on properties. They are further divided in:
-    - unguided: they exist to let the fuzzer try novel or unexpected interactions, and potentially transition to unexpectedly invalid states
-    - guided: they have the goal of quickly covering code and moving the protocol to known valid states (eg: by moving funds between valid users)
-- `property_`: they only assert the protocol is in a valid state, without causing a state transition. Note that they still use assertion-mode testing for simplicity, but could be migrated to run in property-mode.

From 15f6f4a1ae6b96c575d7f19d1ba9193477ad65d8 Mon Sep 17 00:00:00 2001
From: teddy <teddy@defi.sucks>
Date: Mon, 2 Sep 2024 17:02:24 -0300
Subject: [PATCH 10/13] chore: delete medusa config

---
 packages/contracts-bedrock/medusa.json | 86 --------------------------
 1 file changed, 86 deletions(-)
 delete mode 100644 packages/contracts-bedrock/medusa.json

diff --git a/packages/contracts-bedrock/medusa.json b/packages/contracts-bedrock/medusa.json
deleted file mode 100644
index 44e271c4ca34..000000000000
--- a/packages/contracts-bedrock/medusa.json
+++ /dev/null
@@ -1,86 +0,0 @@
-{
-	"fuzzing": {
-		"workers": 10,
-		"workerResetLimit": 50,
-		"timeout": 0,
-		"testLimit": 0,
-		"callSequenceLength": 100,
-		"corpusDirectory": "test/properties/medusa/corpus/",
-		"coverageEnabled": true,
-		"targetContracts": ["ProtocolProperties"],
-		"targetContractsBalances": [],
-		"constructorArgs": {},
-		"deployerAddress": "0x30000",
-		"senderAddresses": [
-			"0x10000",
-			"0x20000",
-			"0x30000"
-		],
-		"blockNumberDelayMax": 60480,
-		"blockTimestampDelayMax": 604800,
-		"blockGasLimit": 30000000,
-		"transactionGasLimit": 12500000,
-		"testing": {
-			"stopOnFailedTest": true,
-			"stopOnFailedContractMatching": false,
-			"stopOnNoTests": true,
-			"testAllContracts": false,
-			"traceAll": true,
-			"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": [
-        "ProtocolProperties.test_ERC20external_zeroAddressBalance()",
-        "ProtocolProperties.test_ERC20external_transferToZeroAddress()",
-        "ProtocolProperties.test_ERC20external_transferFromToZeroAddress(uint256)"
-      ]
-		},
-		"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
-	}
-}

From 10d8a305da0a4f9f51846627a86ed8462ebc4ab6 Mon Sep 17 00:00:00 2001
From: teddy <teddy@defi.sucks>
Date: Tue, 3 Sep 2024 18:20:47 -0300
Subject: [PATCH 11/13] docs: limited support for subdirectories in
 test/invariant

---
 .../scripts/autogen/generate-invariant-docs/main.go         | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/packages/contracts-bedrock/scripts/autogen/generate-invariant-docs/main.go b/packages/contracts-bedrock/scripts/autogen/generate-invariant-docs/main.go
index f408095483b3..38a0b2e3d166 100644
--- a/packages/contracts-bedrock/scripts/autogen/generate-invariant-docs/main.go
+++ b/packages/contracts-bedrock/scripts/autogen/generate-invariant-docs/main.go
@@ -76,6 +76,12 @@ func docGen(invariantsDir, docsDir string) error {
 		// Read the contents of the invariant test file.
 		fileName := file.Name()
 		filePath := filepath.Join(invariantsDir, fileName)
+		// where invariants for a module have their own directory, interpret
+		// the test file with the same name as the directory as a 'main' of
+		// sorts, from where documentation is pulled
+		if file.IsDir() {
+			filePath = filepath.Join(filePath, strings.Join([]string{fileName, ".t.sol"}, ""))
+		}
 		fileContents, err := os.ReadFile(filePath)
 		if err != nil {
 			return fmt.Errorf("error reading file %q: %w", filePath, err)

From 827ac0acddb6ee7a62e16a3a175e4fcfc59aa64d Mon Sep 17 00:00:00 2001
From: teddy <teddy@defi.sucks>
Date: Tue, 3 Sep 2024 18:21:23 -0300
Subject: [PATCH 12/13] chore: rename contracts to be more sneaky about medusa

---
 .../OptimismSuperchainERC20/OptimismSuperchainERC20.t.sol       | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/OptimismSuperchainERC20.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/OptimismSuperchainERC20.t.sol
index 06d4768ccdb9..ee95cb8bbe7b 100644
--- a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/OptimismSuperchainERC20.t.sol
+++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/OptimismSuperchainERC20.t.sol
@@ -18,7 +18,7 @@ import { MockL2ToL2CrossDomainMessenger } from "./helpers/MockL2ToL2CrossDomainM
 
 contract OptimismSuperchainERC20Handler is HandlerGetters, ProtocolGuided, ProtocolUnguided { }
 
-contract OptimismSuperchainERC20MedusaProperties is Test {
+contract OptimismSuperchainERC20Properties is Test {
     OptimismSuperchainERC20Handler internal handler;
     MockL2ToL2CrossDomainMessenger internal constant MESSENGER =
         MockL2ToL2CrossDomainMessenger(Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER);

From 0b39ae7055beaab69ba77da3576f9cfe77117441 Mon Sep 17 00:00:00 2001
From: teddy <teddy@defi.sucks>
Date: Tue, 3 Sep 2024 18:22:33 -0300
Subject: [PATCH 13/13] docs: rewrite invariant docs in a way compliant with
 autogen scripts

---
 .../invariant-docs/OptimismSuperchainERC20.md      | 14 ++++++++++----
 .../OptimismSuperchainERC20.t.sol                  | 12 ++++++------
 2 files changed, 16 insertions(+), 10 deletions(-)

diff --git a/packages/contracts-bedrock/invariant-docs/OptimismSuperchainERC20.md b/packages/contracts-bedrock/invariant-docs/OptimismSuperchainERC20.md
index 0e3150624da5..7dd70286a4e9 100644
--- a/packages/contracts-bedrock/invariant-docs/OptimismSuperchainERC20.md
+++ b/packages/contracts-bedrock/invariant-docs/OptimismSuperchainERC20.md
@@ -1,10 +1,16 @@
 # `OptimismSuperchainERC20` Invariants
 
-## Calls to sendERC20 should always succeed as long as the actor has enough balance. Actor's balance should also not increase out of nowhere but instead should decrease by the amount sent.
-**Test:** [`OptimismSuperchainERC20.t.sol#L194`](../test/invariants/OptimismSuperchainERC20.t.sol#L194)
+## sum of supertoken total supply across all chains is always <= to convert(legacy, super)- convert(super, legacy)
+**Test:** [`OptimismSuperchainERC20#L36`](../test/invariants/OptimismSuperchainERC20#L36)
 
 
 
-## Calls to relayERC20 should always succeeds when a message is received from another chain. Actor's balance should only increase by the amount relayed.
-**Test:** [`OptimismSuperchainERC20.t.sol#L212`](../test/invariants/OptimismSuperchainERC20.t.sol#L212)
+## sum of supertoken total supply across all chains is equal to convert(legacy, super)- convert(super, legacy) when all when all cross-chain messages are processed
+**Test:** [`OptimismSuperchainERC20#L57`](../test/invariants/OptimismSuperchainERC20#L57)
 
+
+
+## many other assertion mode invariants are also defined  under `test/invariants/OptimismSuperchainERC20/fuzz/` .
+**Test:** [`OptimismSuperchainERC20#L79`](../test/invariants/OptimismSuperchainERC20#L79)
+
+since setting`fail_on_revert=false` also ignores StdAssertion failures, this invariant explicitly asks the handler for assertion test failures 
\ No newline at end of file
diff --git a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/OptimismSuperchainERC20.t.sol b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/OptimismSuperchainERC20.t.sol
index ee95cb8bbe7b..d4662277fbd2 100644
--- a/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/OptimismSuperchainERC20.t.sol
+++ b/packages/contracts-bedrock/test/invariants/OptimismSuperchainERC20/OptimismSuperchainERC20.t.sol
@@ -30,8 +30,7 @@ contract OptimismSuperchainERC20Properties is Test {
 
     // TODO: will need rework after
     //   - `convert`
-    /// @custom:property-id 19
-    /// @custom:property sum of supertoken total supply across all chains is always <= to convert(legacy, super)-
+    /// @custom:invariant sum of supertoken total supply across all chains is always <= to convert(legacy, super)-
     /// convert(super, legacy)
     function invariant_totalSupplyAcrossChainsEqualsMintsMinusFundsInTransit() external view {
         // iterate over unique deploy salts aka supertokens that are supposed to be compatible with each other
@@ -52,8 +51,7 @@ contract OptimismSuperchainERC20Properties is Test {
 
     // TODO: will need rework after
     //   - `convert`
-    /// @custom:property-id 21
-    /// @custom:property sum of supertoken total supply across all chains is equal to convert(legacy, super)-
+    /// @custom:invariant sum of supertoken total supply across all chains is equal to convert(legacy, super)-
     /// convert(super, legacy) when all when all cross-chain messages are processed
     function invariant_totalSupplyAcrossChainsEqualsMintsWhenQueueIsEmpty() external view {
         if (MESSENGER.messageQueueLength() != 0) {
@@ -74,8 +72,10 @@ contract OptimismSuperchainERC20Properties is Test {
         }
     }
 
-    ///@notice `fail_on_revert=false` also ignores StdAssertion failures, so we
-    /// can't simply override compatibleAssert to call StdAssertions.assertTrue
+    /// @custom:invariant many other assertion mode invariants are also defined  under `test/invariants/OptimismSuperchainERC20/fuzz/` .
+    ///
+    ///     since setting`fail_on_revert=false` also ignores StdAssertion failures, this invariant explicitly asks the
+    ///     handler for assertion test failures
     function invariant_handlerAssertions() external view {
         assertFalse(handler.failed());
     }