feat: add crosschain properties #24
Closed
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| uint256 _totalSupplyBefore = optimismSuperchainERC20.totalSupply(); | ||
| uint256 _fromBalanceBefore = optimismSuperchainERC20.balanceOf(_from); | ||
| uint256 _totalSupplyBefore = sourceToken.totalSupply(); | ||
| uint256 _fromBalanceBefore = sourceToken.balanceOf(_from); |
0xteddybear
reviewed
Aug 20, 2024
packages/contracts-bedrock/test/properties/halmos/MockL2ToL2Messenger.sol
Show resolved
Hide resolved
| @@ -28,23 +42,24 @@ contract MockL2ToL2Messenger is IL2ToL2CrossDomainMessenger { | |||
| address _target, | |||
| bytes calldata _message | |||
| ) | |||
| external | |||
| public | |||
0xDiscotech
changed the base branch from
feat/halmos-symbolic-tests
to
feat/invariant-testing
0xDiscotech
force-pushed
the
feat/add-crosschain-properties
branch
from
608e74a to
2239e0f
Compare
* refactor: allow for atomicity on mock messenger * refactor: cross domain sender logic on mock messenger * refactor: l2 to l2 caller and messenge sender logic * chore: remove assumes for removed checks on mock messenger
0xteddybear
force-pushed
the
feat/add-crosschain-properties
branch
from
2239e0f to
773a1d8
Compare
0xteddybear
reviewed
Aug 26, 2024
| @@ -89,21 +114,18 @@ contract SymTest_OptimismSuperchainERC20 is SymTest, HalmosBase { | |||
| vm.assume(_to != address(0)); | |||
| // Deploying a new messenger because of an issue of not being able to etch the storage layout of the mock | |||
| // contract. So needed to a new one setting the symbolic immutable variable for the crossDomainSender. | |||
| vm.etch(address(MESSENGER), address(new MockL2ToL2Messenger(_crossDomainSender)).code); | |||
| // Used 0 address on source token so when the `soureToken` calls it if returns the symbolic `_crossDomainSender` | |||
There was a problem hiding this comment.
debugging this must've been the opposite of fun 😁
| @@ -5,6 +5,7 @@ import { Test } from "forge-std/Test.sol"; | |||
|
|
|||
| contract HalmosBase is Test { | |||
| uint256 internal constant CURRENT_CHAIN_ID = 1; | |||
| uint256 internal constant DESTINATION_CHAIN_ID = 2; | |||
|
This PR is stale because it has been open 14 days with no activity. Remove stale label or comment or this will be closed in 5 days. |
|
The symbolic tests will be written and proved using Kontrol instead |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
refactor: allow for atomicity on mock messenger
refactor: cross domain sender logic on mock messenger
refactor: l2 to l2 caller and messenge sender logic
chore: remove assumes for removed checks on mock messenger
On the mock messenger, I had to return immutable vars on cross domain sender function due to the same problem with the storage layout. The same happens with the destination chain value on
sendMessage.To run the files:
just test-halmos-allCLOSES FUZZ-32