AtHeartEngineer/staking-reward-streamer
1
0
Fork 0
mirror of https://github.com/vacp2p/staking-reward-streamer.git synced 2026-01-09 15:27:55 -05:00
Code Issues Packages Projects Releases Wiki Activity

chore(certora): add rule to test the sum of all distributors allocation

Browse Source
This commit is contained in:
Andrea Franz
2025-03-11 13:08:31 +01:00
parent 26926c1d5e
commit 1f6b6c1c07
4 changed files with 190 additions and 172 deletions
Download Patch File Download Diff File Expand all files Collapse all files

150
.gas-report
View File

@@ -10,7 +10,7 @@
|-------------------------------------------------------------------------------------------+-----------------+--------+--------+--------+---------|
| Function Name | Min | Avg | Median | Max | # Calls |
|-------------------------------------------------------------------------------------------+-----------------+--------+--------+--------+---------|
| fallback | 746 | 132652 | 190833 | 190869 | 507 |
| fallback | 5307 | 133628 | 190929 | 190965 | 507 |
╰-------------------------------------------------------------------------------------------+-----------------+--------+--------+--------+---------╯
╭-----------------------------------------------------+-----------------+---------+---------+---------+---------╮
@@ -18,13 +18,13 @@
+===============================================================================================================+
| Deployment Cost | Deployment Size | | | | |
|-----------------------------------------------------+-----------------+---------+---------+---------+---------|
| 4817421 | 23324 | | | | |
| 4821705 | 23344 | | | | |
|-----------------------------------------------------+-----------------+---------+---------+---------+---------|
| | | | | | |
|-----------------------------------------------------+-----------------+---------+---------+---------+---------|
| Function Name | Min | Avg | Median | Max | # Calls |
|-----------------------------------------------------+-----------------+---------+---------+---------+---------|
| run | 4016668 | 4016668 | 4016668 | 4016668 | 110 |
| run | 4020680 | 4020680 | 4020680 | 4020680 | 110 |
╰-----------------------------------------------------+-----------------+---------+---------+---------+---------╯
╭-----------------------------------------------------------+-----------------+---------+---------+---------+---------╮
@@ -55,19 +55,19 @@
| run | 7309252 | 7309252 | 7309252 | 7309252 | 85 |
╰-----------------------------------------------------------------------------+-----------------+---------+---------+---------+---------╯
╭---------------------------------------------------------+-----------------+-----+--------+-----+---------╮
| script/DeploymentConfig.s.sol:DeploymentConfig Contract | | | | | |
+==========================================================================================================+
| Deployment Cost | Deployment Size | | | | |
|---------------------------------------------------------+-----------------+-----+--------+-----+---------|
| 0 | 9183 | | | | |
|---------------------------------------------------------+-----------------+-----+--------+-----+---------|
| | | | | | |
|---------------------------------------------------------+-----------------+-----+--------+-----+---------|
| Function Name | Min | Avg | Median | Max | # Calls |
|---------------------------------------------------------+-----------------+-----+--------+-----+---------|
| activeNetworkConfig | 597 | 597 | 597 | 597 | 320 |
╰---------------------------------------------------------+-----------------+-----+--------+-----+---------╯
╭---------------------------------------------------------+-----------------+------+--------+------+---------╮
| script/DeploymentConfig.s.sol:DeploymentConfig Contract | | | | | |
+============================================================================================================+
| Deployment Cost | Deployment Size | | | | |
|---------------------------------------------------------+-----------------+------+--------+------+---------|
| 0 | 9183 | | | | |
|---------------------------------------------------------+-----------------+------+--------+------+---------|
| | | | | | |
|---------------------------------------------------------+-----------------+------+--------+------+---------|
| Function Name | Min | Avg | Median | Max | # Calls |
|---------------------------------------------------------+-----------------+------+--------+------+---------|
| activeNetworkConfig | 597 | 2753 | 597 | 6597 | 320 |
╰---------------------------------------------------------+-----------------+------+--------+------+---------╯
╭-------------------------------------------------------------------------------+-----------------+---------+---------+---------+---------╮
| script/UpgradeRewardsStreamerMP.s.sol:UpgradeRewardsStreamerMPScript Contract | | | | | |
@@ -88,7 +88,7 @@
+=====================================================================================+
| Deployment Cost | Deployment Size | | | | |
|------------------------------+-----------------+--------+--------+--------+---------|
| 0 | 10027 | | | | |
| 0 | 10047 | | | | |
|------------------------------+-----------------+--------+--------+--------+---------|
| | | | | | |
|------------------------------+-----------------+--------+--------+--------+---------|
@@ -102,23 +102,23 @@
|------------------------------+-----------------+--------+--------+--------+---------|
| approve | 419 | 419 | 419 | 419 | 3 |
|------------------------------+-----------------+--------+--------+--------+---------|
| balanceOf | 4019 | 11685 | 10019 | 21019 | 9 |
| balanceOf | 21019 | 21019 | 21019 | 21019 | 9 |
|------------------------------+-----------------+--------+--------+--------+---------|
| getRewardDistributors | 1140 | 3384 | 3384 | 5628 | 6 |
| getRewardDistributors | 5140 | 7384 | 7384 | 9628 | 6 |
|------------------------------+-----------------+--------+--------+--------+---------|
| initialize | 95872 | 95872 | 95872 | 95872 | 110 |
|------------------------------+-----------------+--------+--------+--------+---------|
| mint | 2654 | 58515 | 74916 | 74916 | 18 |
|------------------------------+-----------------+--------+--------+--------+---------|
| mintAllowance | 7286 | 7322 | 7322 | 7359 | 2 |
| mintAllowance | 28286 | 28322 | 28322 | 28359 | 2 |
|------------------------------+-----------------+--------+--------+--------+---------|
| owner | 363 | 1029 | 363 | 2363 | 3 |
| owner | 2363 | 2363 | 2363 | 2363 | 3 |
|------------------------------+-----------------+--------+--------+--------+---------|
| removeRewardDistributor | 2632 | 12148 | 4824 | 28990 | 9 |
|------------------------------+-----------------+--------+--------+--------+---------|
| setReward | 21947 | 151921 | 164145 | 164145 | 289 |
| setReward | 22043 | 152017 | 164241 | 164241 | 289 |
|------------------------------+-----------------+--------+--------+--------+---------|
| totalSupply | 3827 | 6008 | 3827 | 11827 | 11 |
| totalSupply | 24827 | 24827 | 24827 | 24827 | 11 |
|------------------------------+-----------------+--------+--------+--------+---------|
| transfer | 417 | 417 | 417 | 417 | 3 |
|------------------------------+-----------------+--------+--------+--------+---------|
@@ -144,7 +144,7 @@
|-------------------------------------------------+-----------------+-------+--------+-------+---------|
| isApprovedForAll | 510 | 510 | 510 | 510 | 1 |
|-------------------------------------------------+-----------------+-------+--------+-------+---------|
| metadataGenerator | 325 | 325 | 325 | 325 | 1 |
| metadataGenerator | 2325 | 2325 | 2325 | 2325 | 1 |
|-------------------------------------------------+-----------------+-------+--------+-------+---------|
| safeTransferFrom(address,address,uint256) | 485 | 485 | 485 | 485 | 1 |
|-------------------------------------------------+-----------------+-------+--------+-------+---------|
@@ -154,7 +154,7 @@
|-------------------------------------------------+-----------------+-------+--------+-------+---------|
| setMetadataGenerator | 24036 | 27334 | 28983 | 28983 | 3 |
|-------------------------------------------------+-----------------+-------+--------+-------+---------|
| tokenURI | 68949 | 68949 | 68949 | 68949 | 1 |
| tokenURI | 75449 | 75449 | 75449 | 75449 | 1 |
|-------------------------------------------------+-----------------+-------+--------+-------+---------|
| transferFrom | 530 | 530 | 530 | 530 | 1 |
╰-------------------------------------------------+-----------------+-------+--------+-------+---------╯
@@ -182,41 +182,41 @@
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| enableEmergencyMode | 2543 | 25291 | 25457 | 25457 | 264 |
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| getAccountTotalMaxMP | 3191 | 3191 | 3191 | 3191 | 1 |
| getAccountTotalMaxMP | 21191 | 21191 | 21191 | 21191 | 1 |
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| getAccountTotalStakedBalance | 15170 | 15170 | 15170 | 15170 | 1 |
| getAccountTotalStakedBalance | 21170 | 21170 | 21170 | 21170 | 1 |
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| getAccountVaults | 5230 | 5230 | 5230 | 5230 | 4 |
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| getStakedBalance | 2643 | 2643 | 2643 | 2643 | 1 |
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| getVault | 1970 | 1970 | 1970 | 1970 | 2130 |
| getVault | 17970 | 17970 | 17970 | 17970 | 2130 |
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| initialize | 92753 | 92753 | 92753 | 92753 | 85 |
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| lastRewardTime | 407 | 1407 | 1407 | 2407 | 2 |
| lastRewardTime | 2407 | 2407 | 2407 | 2407 | 2 |
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| leave | 90373 | 90373 | 90373 | 90373 | 1 |
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| lock | 7040 | 69866 | 71758 | 88871 | 1032 |
| lock | 7040 | 69948 | 71758 | 88871 | 1032 |
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| migrateToVault | 13570 | 72264 | 15777 | 187446 | 3 |
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| mpBalanceOf | 917 | 2361 | 2316 | 7063 | 12 |
| mpBalanceOf | 4917 | 8695 | 10316 | 10316 | 12 |
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| mpBalanceOfAccount | 10356 | 10356 | 10356 | 10356 | 1 |
| mpBalanceOfAccount | 32356 | 32356 | 32356 | 32356 | 1 |
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| mpStakedOf | 606 | 759 | 606 | 2606 | 13 |
| mpStakedOf | 2606 | 2606 | 2606 | 2606 | 13 |
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| proxiableUUID | 342 | 342 | 342 | 342 | 3 |
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| registerVault | 2539 | 74492 | 74970 | 74970 | 331 |
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| rewardEndTime | 385 | 1385 | 1385 | 2385 | 2 |
| rewardEndTime | 2385 | 2385 | 2385 | 2385 | 2 |
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| rewardStartTime | 430 | 1430 | 1430 | 2430 | 2 |
| rewardStartTime | 2430 | 2430 | 2430 | 2430 | 2 |
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| rewardsBalanceOf | 2340 | 3544 | 3953 | 6340 | 268 |
| rewardsBalanceOf | 20340 | 24475 | 25953 | 26174 | 268 |
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| setReward | 2508 | 105559 | 107076 | 107076 | 264 |
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
@@ -224,35 +224,35 @@
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| setTrustedCodehash | 24194 | 24194 | 24194 | 24194 | 85 |
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| stake | 2703 | 234576 | 225331 | 246118 | 2377 |
| stake | 2703 | 234532 | 225331 | 246118 | 2377 |
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| totalMP | 805 | 1257 | 1257 | 1710 | 6 |
| totalMP | 6805 | 8257 | 8257 | 9710 | 6 |
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| totalMPAccrued | 385 | 385 | 385 | 385 | 2132 |
| totalMPAccrued | 2385 | 2385 | 2385 | 2385 | 2132 |
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| totalMPStaked | 429 | 429 | 429 | 429 | 2135 |
| totalMPStaked | 2429 | 2429 | 2429 | 2429 | 2135 |
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| totalMaxMP | 407 | 407 | 407 | 407 | 2132 |
| totalMaxMP | 2407 | 2407 | 2407 | 2407 | 2132 |
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| totalRewardsAccrued | 407 | 407 | 407 | 407 | 3 |
| totalRewardsAccrued | 2407 | 2407 | 2407 | 2407 | 3 |
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| totalRewardsSupply | 998 | 1624 | 1792 | 6737 | 290 |
| totalRewardsSupply | 6737 | 11068 | 11792 | 11903 | 290 |
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| totalShares | 662 | 662 | 662 | 662 | 6 |
| totalShares | 4662 | 4662 | 4662 | 4662 | 6 |
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| totalStaked | 408 | 408 | 408 | 408 | 2139 |
| totalStaked | 2408 | 2408 | 2408 | 2408 | 2139 |
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| unstake | 50925 | 75960 | 75829 | 83197 | 269 |
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| updateGlobalState | 15820 | 27822 | 29230 | 29521 | 277 |
| updateGlobalState | 15820 | 27726 | 29230 | 29521 | 277 |
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| updateVaultMP | 25061 | 34609 | 36472 | 36763 | 277 |
| updateVaultMP | 25061 | 34558 | 36472 | 36763 | 277 |
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| upgradeTo | 10235 | 10857 | 10235 | 12723 | 4 |
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| upgradeToAndCall | 3228 | 3228 | 3228 | 3228 | 1 |
|------------------------------------------------------+-----------------+--------+--------+--------+---------|
| vaultShares | 893 | 1059 | 893 | 2893 | 12 |
| vaultShares | 4893 | 4893 | 4893 | 4893 | 12 |
╰------------------------------------------------------+-----------------+--------+--------+--------+---------╯
╭----------------------------------------+-----------------+--------+--------+--------+---------╮
@@ -274,7 +274,7 @@
|----------------------------------------+-----------------+--------+--------+--------+---------|
| leave | 12161 | 126893 | 67285 | 360844 | 4 |
|----------------------------------------+-----------------+--------+--------+--------+---------|
| lock | 12091 | 85259 | 87221 | 104334 | 1033 |
| lock | 12091 | 85341 | 87221 | 104334 | 1033 |
|----------------------------------------+-----------------+--------+--------+--------+---------|
| migrateToVault | 29058 | 98946 | 31265 | 236516 | 3 |
|----------------------------------------+-----------------+--------+--------+--------+---------|
@@ -282,7 +282,7 @@
|----------------------------------------+-----------------+--------+--------+--------+---------|
| register | 12674 | 78142 | 78600 | 78600 | 331 |
|----------------------------------------+-----------------+--------+--------+--------+---------|
| stake | 12071 | 290010 | 280899 | 301686 | 2378 |
| stake | 12071 | 289967 | 280899 | 301686 | 2378 |
|----------------------------------------+-----------------+--------+--------+--------+---------|
| stakeManager | 369 | 369 | 369 | 369 | 330 |
|----------------------------------------+-----------------+--------+--------+--------+---------|
@@ -293,21 +293,21 @@
| withdraw | 20754 | 20754 | 20754 | 20754 | 1 |
╰----------------------------------------+-----------------+--------+--------+--------+---------╯
╭----------------------------------------------------+-----------------+------+--------+--------+---------╮
| src/TransparentProxy.sol:TransparentProxy Contract | | | | | |
+=========================================================================================================+
| Deployment Cost | Deployment Size | | | | |
|----------------------------------------------------+-----------------+------+--------+--------+---------|
| 0 | 1520 | | | | |
|----------------------------------------------------+-----------------+------+--------+--------+---------|
| | | | | | |
|----------------------------------------------------+-----------------+------+--------+--------+---------|
| Function Name | Min | Avg | Median | Max | # Calls |
|----------------------------------------------------+-----------------+------+--------+--------+---------|
| fallback | 708 | 5307 | 853 | 142390 | 12493 |
|----------------------------------------------------+-----------------+------+--------+--------+---------|
| implementation | 346 | 2345 | 2346 | 2346 | 4020 |
╰----------------------------------------------------+-----------------+------+--------+--------+---------╯
╭----------------------------------------------------+-----------------+-------+--------+--------+---------╮
| src/TransparentProxy.sol:TransparentProxy Contract | | | | | |
+==========================================================================================================+
| Deployment Cost | Deployment Size | | | | |
|----------------------------------------------------+-----------------+-------+--------+--------+---------|
| 0 | 1520 | | | | |
|----------------------------------------------------+-----------------+-------+--------+--------+---------|
| | | | | | |
|----------------------------------------------------+-----------------+-------+--------+--------+---------|
| Function Name | Min | Avg | Median | Max | # Calls |
|----------------------------------------------------+-----------------+-------+--------+--------+---------|
| fallback | 5208 | 14160 | 7353 | 142390 | 12493 |
|----------------------------------------------------+-----------------+-------+--------+--------+---------|
| implementation | 2346 | 2346 | 2346 | 2346 | 4020 |
╰----------------------------------------------------+-----------------+-------+--------+--------+---------╯
╭--------------------------------------------+-----------------+--------+--------+--------+---------╮
| src/VaultFactory.sol:VaultFactory Contract | | | | | |
@@ -336,9 +336,9 @@
|------------------------------------------------------------------------------------------+-----------------+-------+--------+-------+---------|
| generate | 54036 | 54036 | 54036 | 54036 | 1 |
|------------------------------------------------------------------------------------------+-----------------+-------+--------+-------+---------|
| imagePrefix | 1183 | 2183 | 2183 | 3183 | 2 |
| imagePrefix | 3183 | 3183 | 3183 | 3183 | 2 |
|------------------------------------------------------------------------------------------+-----------------+-------+--------+-------+---------|
| imageSuffix | 1227 | 2227 | 2227 | 3227 | 2 |
| imageSuffix | 3227 | 3227 | 3227 | 3227 | 2 |
|------------------------------------------------------------------------------------------+-----------------+-------+--------+-------+---------|
| setImageStrings | 25295 | 30634 | 30634 | 35974 | 2 |
╰------------------------------------------------------------------------------------------+-----------------+-------+--------+-------+---------╯
@@ -358,9 +358,9 @@
|------------------------------------------------------------------------------------------+-----------------+-------+--------+-------+---------|
| setURLStrings | 25463 | 30802 | 30802 | 36142 | 2 |
|------------------------------------------------------------------------------------------+-----------------+-------+--------+-------+---------|
| urlPrefix | 1184 | 1184 | 1184 | 1184 | 1 |
| urlPrefix | 3184 | 3184 | 3184 | 3184 | 1 |
|------------------------------------------------------------------------------------------+-----------------+-------+--------+-------+---------|
| urlSuffix | 1228 | 1228 | 1228 | 1228 | 1 |
| urlSuffix | 3228 | 3228 | 3228 | 3228 | 1 |
╰------------------------------------------------------------------------------------------+-----------------+-------+--------+-------+---------╯
╭-------------------------------------------------------------------+-----------------+-------+--------+-------+---------╮
@@ -374,13 +374,13 @@
|-------------------------------------------------------------------+-----------------+-------+--------+-------+---------|
| Function Name | Min | Avg | Median | Max | # Calls |
|-------------------------------------------------------------------+-----------------+-------+--------+-------+---------|
| rewardsBalanceOfAccount | 549 | 1882 | 2549 | 2549 | 18 |
| rewardsBalanceOfAccount | 2549 | 2549 | 2549 | 2549 | 18 |
|-------------------------------------------------------------------+-----------------+-------+--------+-------+---------|
| setTotalKarmaShares | 43589 | 43589 | 43589 | 43589 | 26 |
|-------------------------------------------------------------------+-----------------+-------+--------+-------+---------|
| setUserKarmaShare | 44194 | 44194 | 44194 | 44194 | 6 |
|-------------------------------------------------------------------+-----------------+-------+--------+-------+---------|
| totalRewardsSupply | 324 | 990 | 324 | 2324 | 90 |
| totalRewardsSupply | 324 | 1568 | 2324 | 2324 | 90 |
╰-------------------------------------------------------------------+-----------------+-------+--------+-------+---------╯
╭---------------------------------------------------------------------+-----------------+-------+--------+-------+---------╮
@@ -394,7 +394,7 @@
|---------------------------------------------------------------------+-----------------+-------+--------+-------+---------|
| Function Name | Min | Avg | Median | Max | # Calls |
|---------------------------------------------------------------------+-----------------+-------+--------+-------+---------|
| generate | 58281 | 58281 | 58281 | 58281 | 1 |
| generate | 60281 | 60281 | 60281 | 60281 | 1 |
╰---------------------------------------------------------------------+-----------------+-------+--------+-------+---------╯
╭---------------------------------------------+-----------------+-------+--------+-------+---------╮
@@ -408,11 +408,11 @@
|---------------------------------------------+-----------------+-------+--------+-------+---------|
| Function Name | Min | Avg | Median | Max | # Calls |
|---------------------------------------------+-----------------+-------+--------+-------+---------|
| approve | 29075 | 31592 | 29243 | 46259 | 2377 |
| approve | 29075 | 31593 | 29243 | 46259 | 2377 |
|---------------------------------------------+-----------------+-------+--------+-------+---------|
| balanceOf | 561 | 924 | 561 | 2561 | 2930 |
| balanceOf | 2561 | 2561 | 2561 | 2561 | 2930 |
|---------------------------------------------+-----------------+-------+--------+-------+---------|
| mint | 33964 | 37277 | 34132 | 68248 | 2389 |
| mint | 33964 | 37278 | 34144 | 68248 | 2389 |
╰---------------------------------------------+-----------------+-------+--------+-------+---------╯
╭-----------------------------------------------------------------------------+-----------------+--------+--------+--------+---------╮

188
.gas-snapshot
View File

@@ -1,131 +1,131 @@
CompoundTest:test_RevertWhenInsufficientMPBalance() (gas: 382672)
EmergencyExitTest:test_CannotEnableEmergencyModeTwice() (gas: 93554)
EmergencyExitTest:test_CannotLeaveBeforeEmergencyMode() (gas: 355576)
EmergencyExitTest:test_EmergencyExitBasic() (gas: 448287)
EmergencyExitTest:test_EmergencyExitMultipleUsers() (gas: 772010)
EmergencyExitTest:test_EmergencyExitToAlternateAddress() (gas: 453816)
EmergencyExitTest:test_EmergencyExitWithLock() (gas: 450737)
EmergencyExitTest:test_EmergencyExitWithRewards() (gas: 438773)
EmergencyExitTest:test_EmergencyExitBasic() (gas: 549287)
EmergencyExitTest:test_EmergencyExitMultipleUsers() (gas: 987010)
EmergencyExitTest:test_EmergencyExitToAlternateAddress() (gas: 503816)
EmergencyExitTest:test_EmergencyExitWithLock() (gas: 469737)
EmergencyExitTest:test_EmergencyExitWithRewards() (gas: 504273)
EmergencyExitTest:test_OnlyOwnerCanEnableEmergencyMode() (gas: 39133)
FuzzTests:testFuzz_AccrueMP(uint256,uint256,uint16) (runs: 1000, μ: 524420, ~: 518644)
FuzzTests:testFuzz_AccrueMP_Relock(uint256,uint256,uint16) (runs: 1000, μ: 547640, ~: 549760)
FuzzTests:testFuzz_EmergencyExit(uint256,uint256) (runs: 1000, μ: 514390, ~: 505361)
FuzzTests:testFuzz_Lock(uint256,uint256) (runs: 1000, μ: 526481, ~: 526492)
FuzzTests:testFuzz_Relock(uint256,uint256,uint256) (runs: 1000, μ: 547359, ~: 553885)
FuzzTests:testFuzz_Rewards(uint256,uint256,uint256,uint16,uint16) (runs: 1000, μ: 612241, ~: 613538)
FuzzTests:testFuzz_Stake(uint256,uint256) (runs: 1000, μ: 407701, ~: 398672)
FuzzTests:testFuzz_Unstake(uint256,uint256,uint16,uint256) (runs: 1000, μ: 533986, ~: 533515)
IntegrationTest:testStakeFoo() (gas: 1425242)
KarmaMintAllowanceTest:testAddKarmaDistributorOnlyOwner() (gas: 364780)
KarmaMintAllowanceTest:testBalanceOf() (gas: 443836)
KarmaMintAllowanceTest:testBalanceOfWithNoSystemTotalKarma() (gas: 49501)
KarmaMintAllowanceTest:testMintAllowance_Available() (gas: 355546)
KarmaMintAllowanceTest:testMintAllowance_NotAvailable() (gas: 355551)
KarmaMintAllowanceTest:testMintOnlyOwner() (gas: 397793)
KarmaMintAllowanceTest:testMint_Ok() (gas: 425459)
KarmaMintAllowanceTest:testMint_RevertWithAllowanceExceeded() (gas: 405516)
KarmaMintAllowanceTest:testRemoveKarmaDistributorOnlyOwner() (gas: 88855)
FuzzTests:testFuzz_AccrueMP(uint256,uint256,uint16) (runs: 1000, μ: 604556, ~: 599265)
FuzzTests:testFuzz_AccrueMP_Relock(uint256,uint256,uint16) (runs: 1000, μ: 630345, ~: 632260)
FuzzTests:testFuzz_EmergencyExit(uint256,uint256) (runs: 1000, μ: 609193, ~: 600343)
FuzzTests:testFuzz_Lock(uint256,uint256) (runs: 1000, μ: 606490, ~: 606492)
FuzzTests:testFuzz_Relock(uint256,uint256,uint256) (runs: 1000, μ: 718635, ~: 724885)
FuzzTests:testFuzz_Rewards(uint256,uint256,uint256,uint16,uint16) (runs: 1000, μ: 662953, ~: 665626)
FuzzTests:testFuzz_Stake(uint256,uint256) (runs: 1000, μ: 487504, ~: 478654)
FuzzTests:testFuzz_Unstake(uint256,uint256,uint16,uint256) (runs: 1000, μ: 613994, ~: 613640)
IntegrationTest:testStakeFoo() (gas: 2475242)
KarmaMintAllowanceTest:testAddKarmaDistributorOnlyOwner() (gas: 373280)
KarmaMintAllowanceTest:testBalanceOf() (gas: 468028)
KarmaMintAllowanceTest:testBalanceOfWithNoSystemTotalKarma() (gas: 69501)
KarmaMintAllowanceTest:testMintAllowance_Available() (gas: 383738)
KarmaMintAllowanceTest:testMintAllowance_NotAvailable() (gas: 383743)
KarmaMintAllowanceTest:testMintOnlyOwner() (gas: 449985)
KarmaMintAllowanceTest:testMint_Ok() (gas: 485651)
KarmaMintAllowanceTest:testMint_RevertWithAllowanceExceeded() (gas: 405708)
KarmaMintAllowanceTest:testRemoveKarmaDistributorOnlyOwner() (gas: 97355)
KarmaMintAllowanceTest:testRemoveUnknownKarmaDistributor() (gas: 41416)
KarmaMintAllowanceTest:testTotalSupply() (gas: 352013)
KarmaMintAllowanceTest:testTransfersNotAllowed() (gas: 40219)
KarmaMintAllowanceTest:testTotalSupply() (gas: 380205)
KarmaMintAllowanceTest:testTransfersNotAllowed() (gas: 61719)
KarmaNFTTest:testApproveNotAllowed() (gas: 10507)
KarmaNFTTest:testGetApproved() (gas: 10531)
KarmaNFTTest:testIsApprovedForAll() (gas: 10705)
KarmaNFTTest:testSafeTransferNotAllowed() (gas: 10688)
KarmaNFTTest:testSafeTransferWithDataNotAllowed() (gas: 10884)
KarmaNFTTest:testSetApprovalForAllNotAllowed() (gas: 8519)
KarmaNFTTest:testSetMetadataGenerator() (gas: 984525)
KarmaNFTTest:testSetMetadataGenerator() (gas: 986525)
KarmaNFTTest:testSetMetadataGeneratorRevert() (gas: 981085)
KarmaNFTTest:testTokenURI() (gas: 1079810)
KarmaNFTTest:testTokenURI() (gas: 1086310)
KarmaNFTTest:testTransferNotAllowed() (gas: 10701)
KarmaOwnershipTest:testAddKarmaDistributorOnlyOwner() (gas: 364768)
KarmaOwnershipTest:testBalanceOf() (gas: 443806)
KarmaOwnershipTest:testBalanceOfWithNoSystemTotalKarma() (gas: 49479)
KarmaOwnershipTest:testAddKarmaDistributorOnlyOwner() (gas: 373268)
KarmaOwnershipTest:testBalanceOf() (gas: 467998)
KarmaOwnershipTest:testBalanceOfWithNoSystemTotalKarma() (gas: 69479)
KarmaOwnershipTest:testInitialOwner() (gas: 17601)
KarmaOwnershipTest:testMintOnlyOwner() (gas: 397757)
KarmaOwnershipTest:testOwnershipTransfer() (gas: 98047)
KarmaOwnershipTest:testRemoveKarmaDistributorOnlyOwner() (gas: 88820)
KarmaOwnershipTest:testMintOnlyOwner() (gas: 449949)
KarmaOwnershipTest:testOwnershipTransfer() (gas: 124047)
KarmaOwnershipTest:testRemoveKarmaDistributorOnlyOwner() (gas: 97320)
KarmaOwnershipTest:testRemoveUnknownKarmaDistributor() (gas: 41398)
KarmaOwnershipTest:testTotalSupply() (gas: 351983)
KarmaOwnershipTest:testTransfersNotAllowed() (gas: 40196)
KarmaTest:testAddKarmaDistributorOnlyOwner() (gas: 364768)
KarmaTest:testBalanceOf() (gas: 443806)
KarmaTest:testBalanceOfWithNoSystemTotalKarma() (gas: 49545)
KarmaTest:testMintOnlyOwner() (gas: 397757)
KarmaTest:testRemoveKarmaDistributorOnlyOwner() (gas: 88798)
KarmaOwnershipTest:testTotalSupply() (gas: 380175)
KarmaOwnershipTest:testTransfersNotAllowed() (gas: 61696)
KarmaTest:testAddKarmaDistributorOnlyOwner() (gas: 373268)
KarmaTest:testBalanceOf() (gas: 467998)
KarmaTest:testBalanceOfWithNoSystemTotalKarma() (gas: 69545)
KarmaTest:testMintOnlyOwner() (gas: 449949)
KarmaTest:testRemoveKarmaDistributorOnlyOwner() (gas: 97298)
KarmaTest:testRemoveUnknownKarmaDistributor() (gas: 41398)
KarmaTest:testTotalSupply() (gas: 351983)
KarmaTest:testTransfersNotAllowed() (gas: 40241)
LeaveTest:test_LeaveShouldProperlyUpdateAccounting() (gas: 9596127)
KarmaTest:testTotalSupply() (gas: 380175)
KarmaTest:testTransfersNotAllowed() (gas: 61741)
LeaveTest:test_LeaveShouldProperlyUpdateAccounting() (gas: 9746127)
LeaveTest:test_RevertWhenStakeManagerIsTrusted() (gas: 352670)
LeaveTest:test_TrustNewStakeManager() (gas: 9650282)
LockTest:test_LockFailsWithInvalidPeriod(uint256) (runs: 1000, μ: 404127, ~: 404151)
LeaveTest:test_TrustNewStakeManager() (gas: 9661282)
LockTest:test_LockFailsWithInvalidPeriod(uint256) (runs: 1000, μ: 404125, ~: 404151)
LockTest:test_LockFailsWithNoStake() (gas: 109453)
LockTest:test_LockFailsWithZero() (gas: 362797)
LockTest:test_LockMultipleTimesExceedMaxLock() (gas: 687937)
LockTest:test_LockWithPriorLock() (gas: 591117)
LockTest:test_LockWithoutPriorLock() (gas: 469032)
LockTest:test_LockMultipleTimesExceedMaxLock() (gas: 818437)
LockTest:test_LockWithPriorLock() (gas: 717617)
LockTest:test_LockWithoutPriorLock() (gas: 552532)
LockTest:test_RevertWhenVaultToLockIsEmpty() (gas: 109411)
MaliciousUpgradeTest:test_UpgradeStackOverflowStakeManager() (gas: 2018932)
MaliciousUpgradeTest:test_UpgradeStackOverflowStakeManager() (gas: 2080432)
MathTest:test_CalcAbsoluteMaxTotalMP() (gas: 5196)
MathTest:test_CalcAccrueMP() (gas: 8511)
MathTest:test_CalcBonusMP() (gas: 19112)
MathTest:test_CalcBonusMP() (gas: 30612)
MathTest:test_CalcInitialMP() (gas: 5728)
MathTest:test_CalcMaxAccruedMP() (gas: 4842)
MathTest:test_CalcMaxTotalMP() (gas: 19852)
MultipleVaultsStakeTest:test_StakeMultipleVaults() (gas: 860480)
MathTest:test_CalcMaxTotalMP() (gas: 31352)
MultipleVaultsStakeTest:test_StakeMultipleVaults() (gas: 977480)
NFTMetadataGeneratorSVGTest:testGenerateMetadata() (gas: 91375)
NFTMetadataGeneratorSVGTest:testSetImageStrings() (gas: 60081)
NFTMetadataGeneratorSVGTest:testSetImageStrings() (gas: 77581)
NFTMetadataGeneratorSVGTest:testSetImageStringsRevert() (gas: 35891)
NFTMetadataGeneratorURLTest:testGenerateMetadata() (gas: 108068)
NFTMetadataGeneratorURLTest:testSetBaseURL() (gas: 50631)
NFTMetadataGeneratorURLTest:testSetBaseURL() (gas: 59131)
NFTMetadataGeneratorURLTest:testSetBaseURLRevert() (gas: 36066)
RewardsStreamerMP_RewardsTest:testRewardsBalanceOf() (gas: 1325868)
RewardsStreamerMP_RewardsTest:testSetRewards() (gas: 224584)
RewardsStreamerMP_RewardsTest:testSetRewards_RevertsBadAmount() (gas: 61186)
RewardsStreamerMP_RewardsTest:testSetRewards_RevertsBadDuration() (gas: 100963)
RewardsStreamerMP_RewardsTest:testRewardsBalanceOf() (gas: 2769560)
RewardsStreamerMP_RewardsTest:testSetRewards() (gas: 275680)
RewardsStreamerMP_RewardsTest:testSetRewards_RevertsBadAmount() (gas: 61282)
RewardsStreamerMP_RewardsTest:testSetRewards_RevertsBadDuration() (gas: 101059)
RewardsStreamerMP_RewardsTest:testSetRewards_RevertsNotAuthorized() (gas: 39344)
RewardsStreamerMP_RewardsTest:testTotalRewardsSupply() (gas: 760653)
StakeTest:test_StakeMultipleAccounts() (gas: 597410)
StakeTest:test_StakeMultipleAccountsAndRewards() (gas: 605858)
StakeTest:test_StakeMultipleAccountsMPIncreasesMaxMPDoesNotChange() (gas: 1033802)
StakeTest:test_StakeMultipleAccountsWithMinLockUp() (gas: 607956)
StakeTest:test_StakeMultipleAccountsWithRandomLockUp() (gas: 629966)
StakeTest:test_StakeOneAccount() (gas: 336901)
StakeTest:test_StakeOneAccountAndRewards() (gas: 345345)
StakeTest:test_StakeOneAccountMPIncreasesMaxMPDoesNotChange() (gas: 612256)
StakeTest:test_StakeOneAccountReachingMPLimit() (gas: 600323)
StakeTest:test_StakeOneAccountWithMaxLockUp() (gas: 354928)
StakeTest:test_StakeOneAccountWithMinLockUp() (gas: 355502)
StakeTest:test_StakeOneAccountWithRandomLockUp() (gas: 355591)
StakeVaultMigrationTest:testMigrateToVault() (gas: 951404)
RewardsStreamerMP_RewardsTest:testTotalRewardsSupply() (gas: 1295345)
StakeTest:test_StakeMultipleAccounts() (gas: 715910)
StakeTest:test_StakeMultipleAccountsAndRewards() (gas: 770858)
StakeTest:test_StakeMultipleAccountsMPIncreasesMaxMPDoesNotChange() (gas: 1439802)
StakeTest:test_StakeMultipleAccountsWithMinLockUp() (gas: 651956)
StakeTest:test_StakeMultipleAccountsWithRandomLockUp() (gas: 680466)
StakeTest:test_StakeOneAccount() (gas: 414901)
StakeTest:test_StakeOneAccountAndRewards() (gas: 469845)
StakeTest:test_StakeOneAccountMPIncreasesMaxMPDoesNotChange() (gas: 828756)
StakeTest:test_StakeOneAccountReachingMPLimit() (gas: 819323)
StakeTest:test_StakeOneAccountWithMaxLockUp() (gas: 398928)
StakeTest:test_StakeOneAccountWithMinLockUp() (gas: 399502)
StakeTest:test_StakeOneAccountWithRandomLockUp() (gas: 399591)
StakeVaultMigrationTest:testMigrateToVault() (gas: 1239404)
StakeVaultMigrationTest:test_RevertWhenMigrationVaultNotEmpty() (gas: 648781)
StakeVaultMigrationTest:test_RevertWhenNotOwnerOfMigrationVault() (gas: 68131)
StakeVaultTest:testOwner() (gas: 15262)
StakingTokenTest:testOwner() (gas: 15262)
StakingTokenTest:testStakeToken() (gas: 13144)
TrustedCodehashAccessTest:test_RevertWhenProxyCloneCodehashNotTrusted() (gas: 2023465)
UnstakeTest:test_StakeMultipleAccounts() (gas: 597454)
UnstakeTest:test_StakeMultipleAccountsAndRewards() (gas: 605902)
UnstakeTest:test_StakeMultipleAccountsMPIncreasesMaxMPDoesNotChange() (gas: 1033779)
UnstakeTest:test_StakeMultipleAccountsWithMinLockUp() (gas: 607933)
UnstakeTest:test_StakeMultipleAccountsWithRandomLockUp() (gas: 629943)
UnstakeTest:test_StakeOneAccount() (gas: 336901)
UnstakeTest:test_StakeOneAccountAndRewards() (gas: 345389)
UnstakeTest:test_StakeOneAccountMPIncreasesMaxMPDoesNotChange() (gas: 612233)
UnstakeTest:test_StakeOneAccountReachingMPLimit() (gas: 600367)
UnstakeTest:test_StakeOneAccountWithMaxLockUp() (gas: 354950)
UnstakeTest:test_StakeOneAccountWithMinLockUp() (gas: 355524)
UnstakeTest:test_StakeOneAccountWithRandomLockUp() (gas: 355569)
UnstakeTest:test_UnstakeBonusMPAndAccuredMP() (gas: 639843)
UnstakeTest:test_UnstakeMultipleAccounts() (gas: 837910)
UnstakeTest:test_UnstakeMultipleAccountsAndRewards() (gas: 951519)
UnstakeTest:test_UnstakeOneAccount() (gas: 572606)
UnstakeTest:test_UnstakeOneAccountAndAccruedMP() (gas: 597765)
UnstakeTest:test_UnstakeOneAccountAndRewards() (gas: 493843)
UnstakeTest:test_UnstakeOneAccountWithLockUpAndAccruedMP() (gas: 627465)
UnstakeTest:test_StakeMultipleAccounts() (gas: 715954)
UnstakeTest:test_StakeMultipleAccountsAndRewards() (gas: 770902)
UnstakeTest:test_StakeMultipleAccountsMPIncreasesMaxMPDoesNotChange() (gas: 1439779)
UnstakeTest:test_StakeMultipleAccountsWithMinLockUp() (gas: 651933)
UnstakeTest:test_StakeMultipleAccountsWithRandomLockUp() (gas: 680443)
UnstakeTest:test_StakeOneAccount() (gas: 414901)
UnstakeTest:test_StakeOneAccountAndRewards() (gas: 469889)
UnstakeTest:test_StakeOneAccountMPIncreasesMaxMPDoesNotChange() (gas: 828733)
UnstakeTest:test_StakeOneAccountReachingMPLimit() (gas: 819367)
UnstakeTest:test_StakeOneAccountWithMaxLockUp() (gas: 398950)
UnstakeTest:test_StakeOneAccountWithMinLockUp() (gas: 399524)
UnstakeTest:test_StakeOneAccountWithRandomLockUp() (gas: 399569)
UnstakeTest:test_UnstakeBonusMPAndAccuredMP() (gas: 824343)
UnstakeTest:test_UnstakeMultipleAccounts() (gas: 1094410)
UnstakeTest:test_UnstakeMultipleAccountsAndRewards() (gas: 1387019)
UnstakeTest:test_UnstakeOneAccount() (gas: 794606)
UnstakeTest:test_UnstakeOneAccountAndAccruedMP() (gas: 776765)
UnstakeTest:test_UnstakeOneAccountAndRewards() (gas: 706843)
UnstakeTest:test_UnstakeOneAccountWithLockUpAndAccruedMP() (gas: 778965)
UpgradeTest:test_RevertWhenNotOwner() (gas: 3552019)
UpgradeTest:test_UpgradeStakeManager() (gas: 9486252)
VaultRegistrationTest:test_VaultRegistration() (gas: 62962)
UpgradeTest:test_UpgradeStakeManager() (gas: 9572252)
VaultRegistrationTest:test_VaultRegistration() (gas: 89962)
WithdrawTest:testOwner() (gas: 15296)
WithdrawTest:test_CannotWithdrawStakedFunds() (gas: 368382)
WithdrawTest:test_CannotWithdrawStakedFunds() (gas: 392882)

22
certora/specs/Karma.spec
View File

@@ -3,12 +3,30 @@ using Karma as karma;
methods {
function owner() external returns (address) envfree;
function totalDistributorAllocation() external returns (uint256) envfree;
function _.setReward(uint256, uint256) external => HAVOC_ECF;
}
persistent ghost mathint sumOfDistributorAllocations {
init_state axiom sumOfDistributorAllocations == 0;
}
hook Sstore rewardDistributorAllocations[KEY address addr] uint256 newValue (uint256 oldValue) {
sumOfDistributorAllocations = sumOfDistributorAllocations - oldValue + newValue;
}
invariant totalDistributorAllocationIsSumOfDistributorAllocations()
to_mathint(totalDistributorAllocation()) == sumOfDistributorAllocations
filtered {
f -> !isUpgradeFunction(f)
}
// TODO:
// totalDistributorAllocation == sum of all distributor allocations
// sum of external supply <= total supply
definition isUpgradeFunction(method f) returns bool = (
f.selector == sig:karma.upgradeToAndCall(address, bytes).selector
);
definition isERC20TransferFunction(method f) returns bool = (
f.selector == sig:karma.transfer(address, uint256).selector
|| f.selector == sig:karma.transferFrom(address, address, uint256).selector
@@ -46,7 +64,7 @@ rule ownableFuncsOnlyCallableByOwner(method f) {
}
rule totalDistributorAllocationCanOnlyIncrease(method f) filtered { f ->
f.selector != sig:karma.upgradeToAndCall(address, bytes).selector
!isUpgradeFunction(f)
&& !isERC20TransferFunction(f)
} {
env e;

2
src/Karma.sol
View File

@@ -102,7 +102,7 @@ contract Karma is Initializable, ERC20Upgradeable, Ownable2StepUpgradeable, UUPS
revert Karma__UnknownDistributor();
}
rewardDistributorAllocations[rewardsDistributor] = amount;
rewardDistributorAllocations[rewardsDistributor] += amount;
totalDistributorAllocation += amount;
IRewardDistributor(rewardsDistributor).setReward(amount, duration);
}