logos-co
/
staking
mirror of https://github.com/logos-co/staking.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity
staking/certora/confs/StakeManagerProcess.conf

23 lines
560 B
Plaintext
Raw Normal View History

chore(StakeManagerProcessAccount.spec): add specs for processAccount This primarily adds a rule that ensures that, when an account's `balance` changes, `_processAccount()` must have been called as well. There's very few exceptions where an account's `balance` can change without the need of `_processAccount()` but those functions have been deliberately excluded from the rule.
2024-03-13 11:36:58 +00:00
{
feat(StakeManager): implement multiplier points estimation This commit introduces the internal accounting logic for accrueing multiplier points, that will later be used to determine how many experience points an account is eligible to. The majority of the work here was done by @3esmit.
2024-09-04 07:54:45 +00:00
"files":
chore(StakeManagerProcessAccount.spec): add specs for processAccount This primarily adds a rule that ensures that, when an account's `balance` changes, `_processAccount()` must have been called as well. There's very few exceptions where an account's `balance` can change without the need of `_processAccount()` but those functions have been deliberately excluded from the rule.
2024-03-13 11:36:58 +00:00
["contracts/StakeManager.sol",
feat(StakeManager): implement multiplier points estimation This commit introduces the internal accounting logic for accrueing multiplier points, that will later be used to determine how many experience points an account is eligible to. The majority of the work here was done by @3esmit.
2024-09-04 07:54:45 +00:00
"certora/helpers/ERC20A.sol",
"certora/helpers/StakeRewardEstimateA.sol"
chore(StakeManagerProcessAccount.spec): add specs for processAccount This primarily adds a rule that ensures that, when an account's `balance` changes, `_processAccount()` must have been called as well. There's very few exceptions where an account's `balance` can change without the need of `_processAccount()` but those functions have been deliberately excluded from the rule.
2024-03-13 11:36:58 +00:00
],
"link" : [
feat(StakeManager): implement multiplier points estimation This commit introduces the internal accounting logic for accrueing multiplier points, that will later be used to determine how many experience points an account is eligible to. The majority of the work here was done by @3esmit.
2024-09-04 07:54:45 +00:00
"StakeManager:stakedToken=ERC20A",
"StakeManager:stakeRewardEstimate=StakeRewardEstimateA"
chore(StakeManagerProcessAccount.spec): add specs for processAccount This primarily adds a rule that ensures that, when an account's `balance` changes, `_processAccount()` must have been called as well. There's very few exceptions where an account's `balance` can change without the need of `_processAccount()` but those functions have been deliberately excluded from the rule.
2024-03-13 11:36:58 +00:00
],
"msg": "Verifying StakeManager ProcessAccount",
"rule_sanity": "basic",
"verify": "StakeManager:certora/specs/StakeManagerProcessAccount.spec",
"optimistic_loop": true,
"loop_iter": "3",
"packages": [
feat(StakeManager): implement multiplier points estimation This commit introduces the internal accounting logic for accrueing multiplier points, that will later be used to determine how many experience points an account is eligible to. The majority of the work here was done by @3esmit.
2024-09-04 07:54:45 +00:00
"forge-std=lib/forge-std/src",
chore(StakeManagerProcessAccount.spec): add specs for processAccount This primarily adds a rule that ensures that, when an account's `balance` changes, `_processAccount()` must have been called as well. There's very few exceptions where an account's `balance` can change without the need of `_processAccount()` but those functions have been deliberately excluded from the rule.
2024-03-13 11:36:58 +00:00
"@openzeppelin=lib/openzeppelin-contracts"
]
}