diff --git a/packages/contracts-bedrock/test/properties/PROPERTIES.md b/packages/contracts-bedrock/test/properties/PROPERTIES.md index 748d9c306266..fc731a8ac65e 100644 --- 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 index 3f2d13a12bf2..4f2b1ccb819e 100644 --- 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); + } + } }