test: remaining protocol properties #26

0xteddybear · 2024-08-21T00:15:23Z

afaict these are all the supertoken protocol-level properties we can fuzz with an atomic bridge

~~ERC20 properties + state transitions covered in #27 ~~ 🤦 merged it into this branch, feel free to do a partial review of the diff
non-atomic bridge soon ™️

simon-something · 2024-08-23T07:45:50Z

packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol

+
+    /// @custom:property-id 8
+    /// @custom:property calls to sendERC20 with a value of zero dont modify accounting
+    // NOTE: should we keep it? will cause the exact same coverage as property_BridgeSupertoken


indeed, and there is no bound on the amount in bridgeSupertoken, so it's most likely already tested... Wdyt of keeping it separated but explicitely call property_BridgeSupertoken(fromIndex, recipientIndex, destinationChainId, 0) instead (after visibility change)?

simon-something · 2024-08-23T08:23:15Z

packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol

+        try token.relayERC20(currentActor(), recipient, 0) {
+            MESSENGER.setCrossDomainMessageSender(address(0));
+        } catch {
+            MESSENGER.setCrossDomainMessageSender(address(0));
+        }


is the try/catch really needed then?

simon-something · 2024-08-23T08:25:08Z

packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol

+    }
+
+    /// @custom:property-id 7
+    /// @custom:property calls to relayERC20 always succeed as long as the cross-domain caller is valid


the success case isn't tested tho?
should the try have an assert sender==messenger (and catch the opposite), then fuzz the sender?

good find 👀

the relayERC20 call, however, will mint tokens, which without non-atomic bridging will increase the total supply. I have two options for that

track the increase in the appropiate ghost variables (which would kind of mean cheating on property 12)

explicitly revert in the try{} block to discard the state transition

optimistically going for the latter

simon-something · 2024-08-23T08:28:09Z

packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol

+        uint256 amount
+    )
+        external
+        withActor(msg.sender)


for this and next one: are actors optimal when testing access control or similar logic? Or in these case, shouldn't the caller be fuzzed instead (actors then used when there are state related to the address like a balance, approval, etc)?

simon-something

noice, pretty neat, just left a few comment/general q

* chore: add crytic/properties dependency * test: extend protocol properties so it also covers ToB erc20 properties * chore: small linter fixes * docs: update property list * test: handlers for remaining superc20 state transitions * fix: disable ToB properties we are not using and guide the fuzzer a bit more * fix: disable another ToB property not implemented by solady

0xDiscotech

Review in progress!

Questions:

Missing burn, sendERC20 and relayERC20 functions on the handler contract?
Wdyt about using medusa/properties/protocol.t.sol instead of medusa/protocol.properties.t.sol? Or even naming it ProtocolProperties. I'd also remove the .handler on the handlers file.

All of the following points are styling-related and not an issue - they could be addresses on another PR. But they are useful to improve the consistency with the standards to use:
3. Could we define the test for the properties in order incrementally by its id?
4. Could we define the params with _ prefix on the functions?
5. Could we define returned args?
6. Could we use camel case instead of pascal case when defining the tests functions names? e.g. handler_MintSupertoken -> handler_mintSupertoken

0xDiscotech · 2024-08-26T20:20:20Z

packages/contracts-bedrock/test/properties/helpers/Actors.t.sol

+    /// @notice get the currently configured actor, should equal msg.sender
+    function currentActor() internal view returns (address) {
+        return _currentActor;
+    }
+
+    /// @notice get one of the actors by index, useful to get another random
+    /// actor than the one set as currentActor, to perform operations between them
+    function getActorByRawIndex(uint256 rawIndex) internal view returns (address) {
+        return _actors[bound(rawIndex, 0, _actors.length - 1)];
+    }


Just a NIT and really not important since it is a helper. But we could keep sticking to the _ on params and defining the return vars here :)

0xDiscotech · 2024-08-26T20:21:14Z

...ages/contracts-bedrock/test/properties/helpers/OptimismSuperchainERC20ForToBProperties.t.sol

+import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol";
+
+contract OptimismSuperchainERC20ForToBProperties is OptimismSuperchainERC20 {
+    bool public constant isMintableOrBurnable = true;


Suggested change

bool public constant isMintableOrBurnable = true;

bool public constant IS_MINTABLE_OR_BURNABLE = true;

can't do this 😭 it's called by that name by CryticERC20ExternalBasicProperties

I'll add a comment clarifying the reason

0xDiscotech · 2024-08-26T20:21:21Z

...ages/contracts-bedrock/test/properties/helpers/OptimismSuperchainERC20ForToBProperties.t.sol

+
+contract OptimismSuperchainERC20ForToBProperties is OptimismSuperchainERC20 {
+    bool public constant isMintableOrBurnable = true;
+    uint256 public initialSupply = 0;


Suggested change

uint256 public initialSupply = 0;

uint256 public initialSupply;

packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol

0xDiscotech · 2024-08-26T20:41:35Z

packages/contracts-bedrock/test/properties/helpers/Actors.t.sol

+/// @notice helper for tracking actors, taking advantage of the fuzzer already using several `msg.sender`s
+contract Actors is StdUtils {
+    mapping(address => bool) private _isActor;
+    address[] private _actors;


Also, I'd make this public jic you need to loop for the whole array

0xDiscotech · 2024-08-26T20:52:00Z

packages/contracts-bedrock/test/properties/medusa/handlers/Protocol.handler.t.sol

        for (uint256 remoteTokenIndex = 0; remoteTokenIndex < INITIAL_TOKENS; remoteTokenIndex++) {
            _deployRemoteToken();
            for (uint256 supertokenChainId = 0; supertokenChainId < INITIAL_SUPERTOKENS; supertokenChainId++) {


Initializing to = 0; is no needed and can be removed. It is also present in some other parts

0xDiscotech · 2024-08-26T21:56:56Z

packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol

+        fromIndex = bound(fromIndex, 0, allSuperTokens.length - 1);
+        address recipient = getActorByRawIndex(recipientIndex);
+        OptimismSuperchainERC20 token = OptimismSuperchainERC20(allSuperTokens[fromIndex]);
+        uint256 balanceBefore = token.balanceOf(currentActor());


NIT: Missing assertions for to as well

0xDiscotech · 2024-08-26T21:59:37Z

packages/contracts-bedrock/test/properties/medusa/Protocol.properties.t.sol

+    )
+        external
+    {
+        property_BridgeSupertoken(fromIndex, recipientIndex, destinationChainId, 0);


Very nicely handled 👏

doc's idea 🙈

0xteddybear · 2024-08-27T13:44:57Z

Missing burn, sendERC20 and relayERC20 functions on the handler contract?

If I were to add them, I would also have to:

accept they would fail most of the time (not that useful, but we must have some way of letting the fuzzer try things we don't expect)
when they do fail, we should be able to explain why (useful assertions)
when they don't fail, in addition to being able to explain why (another useful assertion) we have to choose between:

require(false), like we do in property_SupERC20RelayERC20AlwaysRevert, to revert the transaction and not bother updating ghost variables (teddy's preference)
repeating the code for ghost variable updates (and perhaps technically break an invariant, like increasing the supply outside of convert)

however, (2) and (3) have useful assertions, which means they don't belong in a handler, but instead in the properties file.

the organization we developed so far is:

handler contract: includes testing suite setup + state transitions that don't require any assertions
properties contract: ideally includes property checks only (think medusa/echidna's property mode), but that's not as powerful as having assertions intertwined with state transitions, so the rule ends up being 'anything with an assertion goes here'

That's why handler_MockNewRemoteToken is in the handler contract (no need to assert anything, yet it modifies the protocol's state), however property_DeployNewSupertoken is in the properties contract since it has a very simple assertion to perform (supertoken supply starting at zero)

Wdyt about using medusa/properties/protocol.t.sol instead of medusa/protocol.properties.t.sol? Or even naming it ProtocolProperties. I'd also remove the .handler on the handlers file.

I wanted to be consistent with horsefacts' weth9 campaign, to be as un-astonishing as possible, but it's true that there's redundancy in having {handler,properties} both in the file and directory names.

All of the above makes me think of a new way to organize the test suite's code:

handlers/Protocol.t.sol: same as current organization, setup + state transitions that don't require assertions
properties/Protocol.guided.t.sol: functions meant to cover a lot of code quickly, by guiding the fuzzer extensively (eg: msg.sender is always pranked to one of the defined actors)
properties/Protocol.unguided.t.sol: functions which will require a lot more calls to cover the same amount of code, but in their lack of guidance might break the system in novel ways (eg: fully fuzzed msg.sender). This is where burn, sendERC20 and relayERC20 handlers you mentioned would live.

what do you think ? (@0xDiscotech @drgorillamd )

0xDiscotech · 2024-08-27T14:40:42Z

@0xteddybear regarding organization, I like the new names and folder structure, but when talking about the guided unguided proposed organization, I don't see a value in separating them. Also because you will need to prank the msg.sender to call burn, sendERC20 and relayERC20 as well.

Also about this:

when they don't fail, in addition to being able to explain why (another useful assertion) we have to choose between:
require(false), like we do in property_SupERC20RelayERC20AlwaysRevert, to revert the transaction and not bother updating ghost variables (teddy's preference)
repeating the code for ghost variable updates (and perhaps technically break an invariant, like increasing the supply outside of convert)

Why should we revert the transaction? Can't we track the states on those calls as well, and then use them when asserting the values? I know it increases the complexity, but we also increase the chances of finding something unexpected IMO.

Btw, the code organization has improved 10x on this PR and this are way clearer right now. Congrats for that.

0xteddybear · 2024-08-29T13:05:09Z

Also because you will need to prank the msg.sender to call burn, sendERC20 and relayERC20 as well

One more clarification regarding this: the difference in guided vs unguided relies on the msg.sender being mocked to a known actor (guided) vs to a fuzzed address (unguided). They are mocked in both.

Btw, the only place where calls are performed from the test contract directly & without mocking is in the ToB properties, and that's why I had to call addActor(address(this)) in the test suite's constructor

0xDiscotech

Way cleaner and organized. Really good job.

I recommend creating a /properties/ folder for the ProtocolProperties contract file.
Also, I see that when defining the fuzz_ tests you use camel case, whereas on property_ test you use pascal case. Is that on purpose? I suggest using camel case.

Ty for the clarification about guided and unguided, makes sense now to me. The paragraph on the doc clearly explains that as well.

0xDiscotech · 2024-08-29T16:22:51Z

packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.guided.t.sol

@@ -150,7 +106,8 @@ contract ProtocolProperties is ProtocolHandler, CryticERC20ExternalBasicProperti
        fromIndex = bound(fromIndex, 0, allSuperTokens.length - 1);
        address recipient = getActorByRawIndex(recipientIndex);
        OptimismSuperchainERC20 token = OptimismSuperchainERC20(allSuperTokens[fromIndex]);
-        uint256 balanceBefore = token.balanceOf(currentActor());
+        uint256 balanceSenderBefore = token.balanceOf(currentActor());
+        uint256 balanceRecipeintBefore = token.balanceOf(recipient);


Suggested change

uint256 balanceRecipeintBefore = token.balanceOf(recipient);

uint256 balanceRecipientBefore = token.balanceOf(recipient);

0xDiscotech

Astonishing job ser 👏

* test: cross-user fuzzed bridges + actor setup * test: fuzz properties 8 and 9 * test: properties 7 and 25 * fix: implement doc's feedback * test: superc20 tob properties (#27) * chore: add crytic/properties dependency * test: extend protocol properties so it also covers ToB erc20 properties * chore: small linter fixes * docs: update property list * test: handlers for remaining superc20 state transitions * fix: disable ToB properties we are not using and guide the fuzzer a bit more * fix: disable another ToB property not implemented by solady * chore: remove zero-initializations * fix: feedback from disco * chore: separate fuzz campaign tests in guided vs unguided * test: dont revert on successful unguided relay * test: add fuzzed calls to burn and mint * docs: document the separation of fuzz test functions * chore: move the properties file to its own directory * chore: consistently use fuzz_ and property_ + camelcase * chore: fix typo * chore: camelcase for handlers as well * fix: revert change that broke halmos campaign compile :D

…11776) * chore: configure medusa with basic supERC20 self-bridging (#19) - used --foundry-compile-all to ensure the test contract under `test/properties` is compiled (otherwise it is not compiled and medusa crashes when it can't find it's compiled representation) - set src,test,script to test/properties/medusa to not waste time compiling contracts that are not required for the medusa campaign - used an atomic bridge, which doesnt allow for testing of several of the proposed invariants fix: delete dead code test: give the fuzzer a head start docs: fix properties order test: document & implement assertions 22, 23 and 24 fix: fixes from self-review test: guide the fuzzer a little bit less previously: initial mint, bound on transfer amount: 146625 calls in 200s now: no initial mint, no bound on transfer amount: 176835 calls in 200s it doesn't seem to slow the fuzzer down fix: fixes after lovely feedback by disco docs: merge both documents and categorized properties by their milestone fix: fixes from parti's review fix: feedback from disco fix: feedback from doc refactor: separate state transitions from pure properties docs: update tested properties refactor: move all assertions into properties contract fix: move function without assertions back into handler test: only use assertion mode fix: improve justfile recipie for medusa * feat: halmos symbolic tests (#21) * feat: introduce OptimismSuperchainERC20 * fix: contract fixes * feat: add snapshots and semver * test: add supports interface tests * test: add invariant test * feat: add parameters to the RelayERC20 event * fix: typo * fix: from param description * fix: event signature and interface pragma * feat: add initializer * feat: use unstructured storage and OZ v5 * feat: update superchain erc20 interfaces * fix: adapt storage to ERC7201 * test: add initializable OZ v5 test * fix: invariant docs * fix: ERC165 implementation * test: improve superc20 invariant (#11) * fix: gas snapshot * chore: configure medusa with basic supERC20 self-bridging - used --foundry-compile-all to ensure the test contract under `test/properties` is compiled (otherwise it is not compiled and medusa crashes when it can't find it's compiled representation) - set src,test,script to test/properties/medusa to not waste time compiling contracts that are not required for the medusa campaign - used an atomic bridge, which doesnt allow for testing of several of the proposed invariants * fix: delete dead code * test: give the fuzzer a head start * feat: create suite for sybolic tests with halmos * test: setup and 3 properties with symbolic tests * chore: remove todo comment * docs: fix properties order * test: document & implement assertions 22, 23 and 24 * fix: fixes from self-review * test: guide the fuzzer a little bit less previously: initial mint, bound on transfer amount: 146625 calls in 200s now: no initial mint, no bound on transfer amount: 176835 calls in 200s it doesn't seem to slow the fuzzer down * feat: add property for burn * refactor: remove symbolic address on mint property * refactor: order the tests based on the property id * feat: checkpoint * chore: set xdomain sender on failing test * chore: enhance mocks * Revert "Merge branch 'chore/setup-medusa' into feat/halmos-symbolic-tests" This reverts commit 945d6b6, reversing changes made to 5dcb3a8. * refactor: remove symbolic addresses to make all of the test work * chore: remove console logs * feat: add properties file * chore: polish * refactor: enhance test on property 7 using direct try catch (now works) * fix: review comments * refactor: add symbolic addresses on test functions * feat: create halmos toml * chore: polish test contract and mock * chore: update property * refactor: move symbolic folder into properties one * feat: create advanced tests helper contract * refactor: enhance tests using symbolic addresses instead of concrete ones * chore: remove 0 property natspec * feat: add halmos profile and just script * chore: rename symbolic folder to halmos * feat: add halmos commands to justfile * chore: reorder assertions on one test * refactor: complete test property seven * chore: mark properties as completed * chore: add halmos-cheatcodes dependency * chore: rename advancedtest->halmosbase * chore: minimize mocked messenger * chore: delete empty halmos file * chore: revert changes to medusa.json * docs: update changes to PROPERTIES.md from base branch * test: sendERC20 destination fix * chore: natspec fixes --------- Co-authored-by: agusduha <[email protected]> Co-authored-by: 0xng <[email protected]> Co-authored-by: teddy <[email protected]> * test: remaining protocol properties (#26) * test: cross-user fuzzed bridges + actor setup * test: fuzz properties 8 and 9 * test: properties 7 and 25 * fix: implement doc's feedback * test: superc20 tob properties (#27) * chore: add crytic/properties dependency * test: extend protocol properties so it also covers ToB erc20 properties * chore: small linter fixes * docs: update property list * test: handlers for remaining superc20 state transitions * fix: disable ToB properties we are not using and guide the fuzzer a bit more * fix: disable another ToB property not implemented by solady * chore: remove zero-initializations * fix: feedback from disco * chore: separate fuzz campaign tests in guided vs unguided * test: dont revert on successful unguided relay * test: add fuzzed calls to burn and mint * docs: document the separation of fuzz test functions * chore: move the properties file to its own directory * chore: consistently use fuzz_ and property_ + camelcase * chore: fix typo * chore: camelcase for handlers as well * fix: revert change that broke halmos campaign compile :D * test: fuzz non atomic bridging (#31) * test: changed mocked messenger ABI for message sending but kept assertions the same * docs: add new properties 26&27 * test: queue cross-chain messages and test related properties * test: relay random messages from queue and check associated invariants * chore: rename bridge->senderc20 method for consistency with relayerc20 * test: not-yet-deployed supertokens can get funds sent to them * chore: medusa runs forever by default doable since it also handles SIGINTs gracefully * chore: document the reason behind relay zero and send zero inconsistencies * fix: feedback from doc * fix: walk around possible medusa issue I'm getting an 'unknown opcode 0x4e' in ProtocolAtomic constructor when calling the MockL2ToL2CrossDomainMessenger for the first time * test: unguided handler for sendERC20 * fix: feedback from disco * chore: remove halmos testsuite * chore: foundry migration (#40) * chore: track assertion failures this is so foundry's invariant contract can check that an assertion returned false in the handler, while still allowing `fail_on_revert = false` so we can still take full advantage of medusa's fuzzer & coverage reports * fix: explicitly skip duplicate supertoken deployments * chore: remove duplicated PROPERTIES.md file * chore: expose data to foundry's external invariant checker * test: run medusa fuzzing campaign from within foundry * fix: eagerly check for duplicate deployments * fix: feedback from doc * chore: shoehorn medusa campaign into foundry dir structure * chore: remove PROPERTIES.md file * chore: delete medusa config * docs: limited support for subdirectories in test/invariant * chore: rename contracts to be more sneaky about medusa * docs: rewrite invariant docs in a way compliant with autogen scripts * chore: fixes from rebase * fix: cleanup superc20 invariants (#46) * chore: revert modifications from medusa campaign * docs: extra docs on why ForTest contract is required * doc: add list of all supertoken properties * chore: run forge fmt * ci: allow for testfiles to be deleted * fix: run doc autogen script after rebase --------- Co-authored-by: Disco <[email protected]> Co-authored-by: agusduha <[email protected]> Co-authored-by: 0xng <[email protected]>

0xteddybear force-pushed the test/state-transitions branch from aa3ccc0 to 72259d2 Compare August 21, 2024 15:00

0xteddybear mentioned this pull request Aug 21, 2024

test: bridge between different accounts #22

Closed

0xteddybear changed the title ~~test: remaining protocol state transitions & properties~~ test: remaining protocol properties Aug 21, 2024

0xteddybear changed the base branch from chore/setup-medusa to feat/invariant-testing August 21, 2024 21:33

0xteddybear requested a review from simon-something August 23, 2024 00:00

simon-something reviewed Aug 23, 2024

View reviewed changes

0xteddybear added 4 commits August 23, 2024 13:30

test: cross-user fuzzed bridges + actor setup

e998667

test: fuzz properties 8 and 9

179fba2

test: properties 7 and 25

6b67194

fix: implement doc's feedback

96ecaad

0xteddybear force-pushed the test/state-transitions branch from 72259d2 to 96ecaad Compare August 23, 2024 18:35

0xteddybear requested a review from simon-something August 23, 2024 18:48

0xDiscotech reviewed Aug 26, 2024

View reviewed changes

0xteddybear added 2 commits August 27, 2024 11:35

chore: remove zero-initializations

5e7eb87

fix: feedback from disco

403dc70

0xteddybear added 3 commits August 28, 2024 19:16

chore: separate fuzz campaign tests in guided vs unguided

dea79ce

test: dont revert on successful unguided relay

7bba3f0

test: add fuzzed calls to burn and mint

cd2b64b

0xteddybear requested a review from 0xDiscotech August 28, 2024 22:28

docs: document the separation of fuzz test functions

231c6b5

0xDiscotech reviewed Aug 29, 2024

View reviewed changes

0xteddybear added 3 commits August 29, 2024 13:45

chore: move the properties file to its own directory

e97fda0

chore: consistently use fuzz_ and property_ + camelcase

b081760

chore: fix typo

8a597a9

0xteddybear requested a review from 0xDiscotech August 29, 2024 16:51

chore: camelcase for handlers as well

e26b9c3

0xDiscotech approved these changes Aug 29, 2024

View reviewed changes

fix: revert change that broke halmos campaign compile :D

c681a7c

0xteddybear merged commit f138b96 into feat/invariant-testing Aug 29, 2024
2 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

test: remaining protocol properties #26

test: remaining protocol properties #26

0xteddybear commented Aug 21, 2024 •

edited

Loading

simon-something Aug 23, 2024

simon-something Aug 23, 2024

simon-something Aug 23, 2024

0xteddybear Aug 23, 2024

simon-something Aug 23, 2024

simon-something left a comment

0xDiscotech left a comment •

edited

Loading

0xDiscotech Aug 26, 2024

0xDiscotech Aug 26, 2024

0xteddybear Aug 27, 2024

0xDiscotech Aug 26, 2024

0xDiscotech Aug 26, 2024

0xDiscotech Aug 26, 2024

0xDiscotech Aug 26, 2024

0xDiscotech Aug 26, 2024

0xteddybear Aug 27, 2024

0xteddybear commented Aug 27, 2024

0xDiscotech commented Aug 27, 2024

0xteddybear commented Aug 29, 2024

0xDiscotech left a comment

0xDiscotech Aug 29, 2024

0xDiscotech left a comment

	bool public constant isMintableOrBurnable = true;
	bool public constant IS_MINTABLE_OR_BURNABLE = true;

	uint256 public initialSupply = 0;
	uint256 public initialSupply;

	uint256 balanceRecipeintBefore = token.balanceOf(recipient);
	uint256 balanceRecipientBefore = token.balanceOf(recipient);

test: remaining protocol properties #26

test: remaining protocol properties #26

Conversation

0xteddybear commented Aug 21, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

simon-something left a comment

Choose a reason for hiding this comment

0xDiscotech left a comment • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

0xteddybear commented Aug 27, 2024

0xDiscotech commented Aug 27, 2024

0xteddybear commented Aug 29, 2024

0xDiscotech left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

0xDiscotech left a comment

Choose a reason for hiding this comment

0xteddybear commented Aug 21, 2024 •

edited

Loading

0xDiscotech left a comment •

edited

Loading