refactor: use symoblic storage cheatcode

packages/contracts-bedrock/kontrol.toml

@@ -0,0 +1,44 @@
+[build.default]
+foundry-project-root       = '.'
+regen                      = false
+rekompile                  = false
+verbose                    = false
+debug                      = false
+auxiliary-lemmas           = true
+
+# require                    = 'lemmas.k'
+# module-import              = 'TestBase:KONTROL-LEMMAS'
+
+[prove.default]
+foundry-project-root       = '.'
+verbose                    = false
+debug                      = false
+max-depth                  = 25000
+reinit                     = false
+cse                        = false
+workers                    = 1
+failure-information        = true
+counterexample-information = true
+minimize-proofs            = false
+fail-fast                  = true
+smt-timeout                = 1000
+break-every-step           = false
+break-on-jumpi             = false
+break-on-calls             = false
+break-on-storage           = false
+break-on-basic-blocks      = false
+break-on-cheatcodes        = false
+run-constructor            = true
+symbolic-immutables        = false
+schedule                   = CANCUN
+init-node-from             = supererc20-state-diff/StateDiff.json
+
+[show.default]
+foundry-project-root       = '.'
+verbose                    = false
+debug                      = false
+use-hex-encoding           = false
+
+[view-kcfg.default]
+foundry-project-root       = '.'
+use-hex-encoding           = false

packages/contracts-bedrock/test/properties/kontrol/FoundryDebugSymbolic.t.sol

@@ -164,10 +164,10 @@ contract FoundryDebugTests is KontrolBase {
 
     function test_proveCrossChainSendERC20() public {
         /* Preconditions */
-        address _from = address(376793390874373408599387495934666716005045108752);
+        address _from = address(728815563385977040452943777879061427756277306519);
         address _to = address(728815563385977040452943777879061427756277306519);
         uint256 _amount = 0;
-        uint256 _chainId = 2;
+        uint256 _chainId = 0;
         // Mint the amount to send
         vm.prank(Predeploys.L2_STANDARD_BRIDGE);
         sourceToken.mint(_from, _amount);
@@ -201,7 +201,7 @@ contract FoundryDebugTests is KontrolBase {
         }
     }
     // VV1__to_114b9705 = 728815563385977040452943777879061427756277306519
-    // VV0__from_114b9705 = 376793390874373408599387495934666716005045108752
+    // VV0__from_114b9705 = 728815563385977040452943777879061427756277306519
     // VV2__amount_114b9705 = 0
-    // VV3__chainId_114b9705 = 2
+    // VV3__chainId_114b9705 = 0
 }

packages/contracts-bedrock/test/properties/kontrol/OptimismSuperchainERC20.k.sol

@@ -92,14 +92,15 @@ contract OptimismSuperchainERC20Kontrol is KontrolBase, InitialState {
         public
     {
         setUpInlined();
+        kevm.symbolicStorage(address(MESSENGER));
 
         /* Preconditions */
         vm.assume(_to != address(0));
         vm.assume(notBuiltinAddress(_from));
         vm.assume(notBuiltinAddress(_to));
         vm.assume(notBuiltinAddress(_sender));
 
-        MESSENGER.forTest_setCustomCrossDomainSender(_crossDomainSender);
+        // MESSENGER.forTest_setCustomCrossDomainSender(_crossDomainSender);
 
         // Expect the cross domain sender to be emitted so after confirming it matches, we can use it for checks
         vm.expectEmit(true, true, true, true);
@@ -109,7 +110,8 @@ contract OptimismSuperchainERC20Kontrol is KontrolBase, InitialState {
         /* Action */
         try sourceToken.relayERC20(_from, _to, _amount) {
             /* Postconditions */
-            assert(_sender == address(MESSENGER) && _crossDomainSender == address(sourceToken));
+            assert(_sender == address(MESSENGER));
+            assert(_crossDomainSender == address(sourceToken));
         } catch {
             // Emit to bypass the check when the call fails
             emit CrossDomainMessageSender(_crossDomainSender);
@@ -125,8 +127,6 @@ contract OptimismSuperchainERC20Kontrol is KontrolBase, InitialState {
         /* Preconditions */
         vm.assume(_to != address(0));
         vm.assume(_to != address(Predeploys.CROSS_L2_INBOX) && _to != address(MESSENGER));
-        // TODO
-        vm.assume(_from != address(0));
 
         vm.assume(notBuiltinAddress(_from));
         vm.assume(notBuiltinAddress(_to));
@@ -254,12 +254,14 @@ contract OptimismSuperchainERC20Kontrol is KontrolBase, InitialState {
     function prove_burn(address _from, uint256 _amount) public {
         setUpInlined();
 
+        kevm.symbolicStorage(address(sourceToken));
+
         /* Preconditions */
         vm.assume(_from != address(0));
         vm.assume(notBuiltinAddress(_from));
 
-        vm.prank(Predeploys.L2_STANDARD_BRIDGE);
-        sourceToken.mint(_from, _amount);
+        // vm.prank(Predeploys.L2_STANDARD_BRIDGE);
+        // sourceToken.mint(_from, _amount);
 
         uint256 _totalSupplyBefore = sourceToken.totalSupply();
         uint256 _balanceBefore = sourceToken.balanceOf(_from);
@@ -291,17 +293,15 @@ contract OptimismSuperchainERC20Kontrol is KontrolBase, InitialState {
     function prove_crossChainSendERC20(address _from, address _to, uint256 _amount, uint256 _chainId) public {
         setUpInlined();
 
+        kevm.symbolicStorage(address(sourceToken));
+
         vm.assume(notBuiltinAddress(_from));
         vm.assume(notBuiltinAddress(_to));
 
         /* Preconditions */
         vm.assume(_to != address(0));
         vm.assume(_from != address(0));
 
-        // Mint the amount to send
-        vm.prank(Predeploys.L2_STANDARD_BRIDGE);
-        sourceToken.mint(_from, _amount);
-
         uint256 fromBalanceBefore = sourceToken.balanceOf(_from);
         uint256 toBalanceBefore = destToken.balanceOf(_to);
         uint256 sourceTotalSupplyBefore = sourceToken.totalSupply();