Certora Acceleration Distributor verification #42
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
|
Created a munged folder where the original code is modified. |
nicholaspai
approved these changes
Dec 22, 2022
Roy-Certora
added a commit
to Certora/across-token
that referenced
this pull request
Jan 19, 2023
* Certora Acceleration Distributor verification (across-protocol#42) * Initial setup for Acceleration Distributor * Updated main spec * README for Acc Distributor * Acc Dist : Update spec and harness * Update spec. Removed Multicaller interface. * improve: Add distributor contract addresses (across-protocol#40) * Bump decode-uri-component from 0.2.0 to 0.2.2 (across-protocol#41) Bumps [decode-uri-component](https://github.com/SamVerschueren/decode-uri-component) from 0.2.0 to 0.2.2. - [Release notes](https://github.com/SamVerschueren/decode-uri-component/releases) - [Commits](SamVerschueren/decode-uri-component@v0.2.0...v0.2.2) --- updated-dependencies: - dependency-name: decode-uri-component dependency-type: indirect ... Signed-off-by: dependabot[bot] <support@github.com> Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> * improve: Update MerkleTree import to be consistent with contracts-v2 (across-protocol#43) MerkleTree currently imported in this repo is out of date with latest in @uma/common and @across-protocol/contracts-v2 * improve: Prepare AD Admin test for updates (across-protocol#46) A pending change will revert on amount=0. This breaks a few tests, so prepare updates for those in advance. * fix: [L-02] Lack of input validation (across-protocol#47) The OZ December 2022 audit identified a lack of input validation on the following functions: - stakeFor() (missing validation of beneficiary address). - unstake() (missing validation on the amount input). - _stake() (missing validation on the amount input). This change applies the missing validation in accordance with the recommendations outlined in the finding. * fix: [L-03] Add missing documentation (across-protocol#53) Add documentation for: - UserDeposit and StakingToken structs. - getAverageDepositTimePostDeposit() - getCurrentTime() - _stake() Update documentation for: - Overall contract. - recoverToken() - stake() - stakeFor() - unstake() - withdrawReward() - exit() - _updateReward() * fix: [L-04] Clamp maxMultiplier lower bound to 1e18 (across-protocol#48) Enforce a minimum 1x multiplier to mitigate the potential for underflow in getUserRewardMultiplier(). There's currently no known use case for a maxMultiplier of less than 1x. * improve: [N-01] Remove redundant event parameter (across-protocol#49) The userRewardsOutstanding value is always set to 0 when emitted, so remove it. * fix: [N-02] Misleading documentation (across-protocol#50) Per an OZ finding, the recoverToken() function specifically checks for whether the token has been initialized; not whether it is currently enabled via staking configuration. * improve: [N-03] Improve style guide conformance (across-protocol#52) * fix: [N-04] Minor typographical errors (across-protocol#51) Based on feedback from OZ. * fix: [L01] Dangerous maximum values for reward calculations (across-protocol#45) * fix: [L01] Dangerous maximum values for reward calculations Signed-off-by: nicholaspai <npai.nyc@gmail.com> * set 1milx max multiplier * Update contracts/AcceleratingDistributor.sol Co-authored-by: Matt Rice <matthewcrice32@gmail.com> * Update AcceleratingDistributor.sol * Update AcceleratingDistributor.Admin.ts Signed-off-by: nicholaspai <npai.nyc@gmail.com> Co-authored-by: Matt Rice <matthewcrice32@gmail.com> Co-authored-by: Paul <108695806+pxrl@users.noreply.github.com> * improve(AD): [M-01] Clarify staking config change implications (across-protocol#55) Relating to the M-01 finding from OpenZeppelin, the proposal is to document the implications of performing various configuration updates to a pre-existing staking token configuration. * fix: Correct residual typographical errors (across-protocol#57) These should have been handled as part of the following commit, but were not: 5254dec * fix: Reinstate docstrings (across-protocol#56) These were erroneously removed in the following commit: be635c4. * refactor(accelerating-distributor): Remove redundant _updateRewards from exit() (across-protocol#44) * refactor(accelerating-distributor): Remove redundant _updateRewards from exit() Refactors withdrawRewards() and unstake() to call internal methods _withdrawRewards() and _unstake() so that exit() only calls _updateRewards() once * Update AcceleratingDistributor.sol * Update AcceleratingDistributor.sol * Update AcceleratingDistributor.sol Signed-off-by: dependabot[bot] <support@github.com> Signed-off-by: nicholaspai <npai.nyc@gmail.com> Co-authored-by: nicholaspai <9457025+nicholaspai@users.noreply.github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> Co-authored-by: Paul <108695806+pxrl@users.noreply.github.com> Co-authored-by: Matt Rice <matthewcrice32@gmail.com>
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.
Includes certora dir with script and spec file.