test: certora spec for RewardsCoordinator #597
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
This comment was marked as off-topic.
This comment was marked as off-topic.
|
|
||
| import "../../src/contracts/core/RewardsCoordinator.sol"; | ||
|
|
||
| contract RewardsCoordinatorHarness is RewardsCoordinator { |
There was a problem hiding this comment.
is there a reason for having a harness here if you aren't adding any functions?
There was a problem hiding this comment.
This was made in case there were any internal functions needed to be made. Looks like we can just remove though
| rule claimWithduplicateTokenLeafs(env e, IRewardsCoordinator.RewardsMerkleClaim claim, address recipient) { | ||
| require claim.tokenLeaves.length == 1; | ||
|
|
||
| checkClaim(e, claim); |
There was a problem hiding this comment.
what's the point of this call?
There was a problem hiding this comment.
Its to ensure that the claim is valid.
since checkClaim doesn't have @withrevert any successful paths of this rule will include checkClaim not reverting. Probably more clear by just having require checkClaim
There was a problem hiding this comment.
makes sense, but adding 'require' syntax would definitely be clearer
| "optimistic_loop": true, | ||
| "optimistic_hashing": true, | ||
| "rule_sanity": "basic", | ||
| "exclude_rule": ["checkClaimNeverFalse"], |
There was a problem hiding this comment.
so is this rule just failing to pass right now then?
There was a problem hiding this comment.
No the rule is called in paymentCoordinatorWithoutSanity.conf. The reason for the separate conf is that this rule fails the sanity check since checkClaim reverts instead of returning false.
|
|
|
||
| processClaim@withrevert(e, claim, recipient); | ||
|
|
||
| assert !lastReverted => canWork; |
There was a problem hiding this comment.
can you assert equality here? that would be stronger if possible; I'm not sure it would work with the summarization of verifyInclusionKeccak though...
There was a problem hiding this comment.
The summarization may be an issue but all other revert reasons will also be problematic. First its things like the contract being paused, in reentrant mode, and >0 msg.value being sent, then compiler checks which are harder to understand.
ChaoticWalrus
approved these changes
Jun 24, 2024
|
Comment on lines
+116
to
+120
| { | ||
| IRewardsCoordinator.RewardsSubmission[] rewardsSubmission1; | ||
| IRewardsCoordinator.RewardsSubmission[] rewardsSubmission2; | ||
| IRewardsCoordinator.RewardsSubmission[] rewardsSubmissions; |
There was a problem hiding this comment.
this rule is checking batch equivalency, right?
|
|
can we close or merge this? @8sunyuan |
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.
Included spec as a github workflow with
certora-prover-conf.yml