feat: test properties 17 and 18

defi-wonderland · Sep 16, 2024 · a4d6cd1 · a4d6cd1
1 parent d0fc92b
commit a4d6cd1
Show file tree

Hide file tree

Showing 2 changed files with 53 additions and 3 deletions.
diff --git a/packages/contracts-bedrock/test/properties/PROPERTIES.md b/packages/contracts-bedrock/test/properties/PROPERTIES.md
@@ -97,8 +97,8 @@ legend:
 
 | id  | milestone           | description                                                                                                                                                           | kontrol | 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                                                                           | [ ]     | [ ]    |
+| 17  | Liquidity Migration | only calls to convert(legacy, super) can increase a supertoken’s total supply and decrease legacy's one across chains                                                 | [ ]     | [ ]    |
+| 18  | Liquidity Migration | only calls to convert(super, legacy) can decrease a supertoken’s total supply and increase the legacy's one 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                   | [ ]     | [ ]    |

diff --git a/packages/contracts-bedrock/test/properties/kontrol/L2StandardBridgeInterop.k.sol b/packages/contracts-bedrock/test/properties/kontrol/L2StandardBridgeInterop.k.sol
@@ -2,7 +2,7 @@
 pragma solidity 0.8.15;
 
 import { Predeploys } from "src/libraries/Predeploys.sol";
-import { L2StandardBridgeInterop } from "src/L2/L2StandardBridgeInterop.sol";
+import "src/L2/L2StandardBridgeInterop.sol";
 import { Test } from "forge-std/Test.sol";
 import { KontrolCheats } from "kontrol-cheatcodes/KontrolCheats.sol";
 import { ERC1967Proxy } from "@openzeppelin/contracts/proxy/ERC1967/ERC1967Proxy.sol";
@@ -227,6 +227,7 @@ contract L2StandardBridgeInteropKontrol is Test, KontrolCheats {
 
         /* Preconditions */
         vm.assume(_sender != address(0));
+
         // Mock the call over `deployments` - not in the scope of the test, but required to avoid a revert
         vm.mockCall(
             Predeploys.OPTIMISM_MINTABLE_ERC20_FACTORY,
@@ -259,4 +260,53 @@ contract L2StandardBridgeInteropKontrol is Test, KontrolCheats {
             assert(superToken.balanceOf(_sender) == superBalanceBefore - _amount);
         }
     }
+
+    /// @custom:property-id 17
+    /// @custom:property Only calls to convert(legacy, super) can increase a supertoken’s total supply
+    /// and decrease legacy's one across chains
+    /// @custom:property-id 18
+    /// @custom:property Only calls to convert(super, legacy) can decrease a supertoken’s total supply and increase
+    /// legacy's one across chains
+    function test_convertUpdatesTotalSupply(bool _legacyIsFrom, address _sender, uint256 _amount) public {
+        setUpInlined();
+
+        /* Preconditions */
+        vm.assume(_sender != address(0));
+
+        // Mock the call over `deployments` - not in the scope of the test, but required to avoid a revert
+        vm.mockCall(
+            Predeploys.OPTIMISM_MINTABLE_ERC20_FACTORY,
+            abi.encodeWithSelector(IOptimismERC20Factory.deployments.selector),
+            abi.encode(REMOTE_TOKEN)
+        );
+        vm.mockCall(
+            Predeploys.OPTIMISM_SUPERCHAIN_ERC20_FACTORY,
+            abi.encodeWithSelector(IOptimismERC20Factory.deployments.selector),
+            abi.encode(REMOTE_TOKEN)
+        );
+
+        // Mint tokens to the sender and get the balances before the conversion
+        vm.prank(address(L2_BRIDGE));
+        if (_legacyIsFrom) legacyToken.mint(_sender, _amount);
+        else superToken.mint(_sender, _amount);
+        uint256 legacyBalanceBefore = legacyToken.balanceOf(_sender);
+        uint256 superBalanceBefore = superToken.balanceOf(_sender);
+
+        vm.startPrank(_sender);
+        /* Action */
+        if (_legacyIsFrom) {
+            L2_BRIDGE.convert(address(legacyToken), address(superToken), _amount);
+
+            /* Postconditions */
+            assert(superToken.totalSupply() == superBalanceBefore + _amount);
+            assert(legacyToken.totalSupply() == legacyBalanceBefore - _amount);
+        } else {
+            /* Action */
+            L2_BRIDGE.convert(address(superToken), address(legacyToken), _amount);
+
+            /* Postconditions */
+            assert(superToken.totalSupply() == superBalanceBefore - _amount);
+            assert(legacyToken.totalSupply() == legacyBalanceBefore + _amount);
+        }
+    }
 }