From aa3ccc027143fb6803fbf19e78d0b4452757ab8b Mon Sep 17 00:00:00 2001
From: teddy <teddy@defi.sucks>
Date: Tue, 20 Aug 2024 21:07:21 -0300
Subject: [PATCH] test: properties 7 and 25

---
 .../test/properties/PROPERTIES.md             |  3 +-
 .../medusa/Protocol.properties.t.sol          | 44 +++++++++++++++++++
 2 files changed, 46 insertions(+), 1 deletion(-)

diff --git a/packages/contracts-bedrock/test/properties/PROPERTIES.md b/packages/contracts-bedrock/test/properties/PROPERTIES.md
index 9023076b9a3d2..6ece63b679923 100644
--- a/packages/contracts-bedrock/test/properties/PROPERTIES.md
+++ b/packages/contracts-bedrock/test/properties/PROPERTIES.md
@@ -70,13 +70,14 @@ legend:
 | 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]    |
-| 7   | SupERC20  | calls to relayERC20 always succeed as long as the cross-domain caller is valid | **[ ]** | [ ]    |
+| 7   | SupERC20  | calls to relayERC20 always succeed as long as the cross-domain caller is valid | **[ ]** | [~]    |
 
 ## Variable transition
 
diff --git a/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol b/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol
index 6b26f83f30f5e..7494d772bc478 100644
--- a/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol
+++ b/packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol
@@ -171,4 +171,48 @@ contract ProtocolProperties is ProtocolHandler {
         assert(balanceBefore == balanceAfter);
         assert(supplyBefore == supplyAfter);
     }
+
+    /// @custom:property-id 7
+    /// @custom:property calls to relayERC20 always succeed as long as the cross-domain caller is valid
+    /// @notice this ensures actors cant simply call relayERC20 and get tokens, no matter the system state
+    /// but there's still some possible work on how hard we can bork the system state with handlers calling
+    /// the L2ToL2CrossDomainMessenger or bridge directly (pending on non-atomic bridging)
+    function property_SupERC20RelayERC20AlwaysRevert(
+        uint256 tokenIndex,
+        address sender,
+        address recipient,
+        uint256 amount
+    )
+        external
+        withActor(msg.sender)
+    {
+        // if msg.sender is the L2ToL2CrossDomainMessenger then this will break other invariants
+        vm.prank(currentActor());
+        try OptimismSuperchainERC20(allSuperTokens[bound(tokenIndex, 0, allSuperTokens.length)]).relayERC20(
+            sender, recipient, amount
+        ) {
+            assert(false);
+        } catch { }
+    }
+
+    /// @custom:property-id 25
+    /// @custom:property supertokens can't be reinitialized
+    function property_SupERC20CantBeReinitialized(
+        uint256 tokenIndex,
+        address remoteToken,
+        string memory name,
+        string memory symbol,
+        uint8 decimals
+    )
+        external
+        withActor(msg.sender)
+    {
+        vm.prank(currentActor());
+        // revert is possible in bound, but is not part of the external call
+        try OptimismSuperchainERC20(allSuperTokens[bound(tokenIndex, 0, allSuperTokens.length)]).initialize(
+            remoteToken, name, symbol, decimals
+        ) {
+            assert(false);
+        } catch { }
+    }
 }