Conversation
|
|
||
| invariant StakingModuleIndexIsIdMinus1(uint256 moduleId) | ||
| getStakingModuleIndexById(moduleId)+1 == getStakingModuleIdById(moduleId) | ||
| //ND : what about moduleIds that are not in the system? Is there some array reference here? looks like a limited-scope rule |
There was a problem hiding this comment.
It's valid for every staking module that is registered in the system. Otherwise, the index of the moduleId is just zero.
|
|
||
| invariant StakingModuleId(uint256 moduleId) | ||
| getStakingModuleIdById(moduleId) == moduleId | ||
| //same comment - is rule sanity passing on the insertion function ? |
There was a problem hiding this comment.
Again, this is only valid for modules that are registered.
I can maybe change the invariant that says ("or moduleId > count => getId == 0")
There was a problem hiding this comment.
that's a much better approach, invariants should not cause vacuity. One should assume that it is also safe to do requireinvariant. in this case it is not
| function safeAssumptions(uint256 moduleId) { | ||
| requireInvariant modulesCountIsLastIndex(); | ||
| if(moduleId > 0) { | ||
| if(moduleId > 0) { //this is strange if you invariants are prove - you can safely assume them |
There was a problem hiding this comment.
One of the invariants here leads to vacuity if the entry is zero.
| env e; | ||
|
|
||
| require getStakingModulesCount() == 0; | ||
| //ND: so is this rule checking first call to addStakingModule ? |
| storage initState = lastStorage; | ||
|
|
||
| addStakingModule(e, name1, Address1, targetShare1, ModuleFee1, TreasuryFee1); | ||
| // ND: why do you need adding name1 ? |
There was a problem hiding this comment.
I should assume any different set of arbitrary arguments, no?
| assert !lastReverted; | ||
| getStakingModuleIdById@withrevert(id); | ||
| assert !lastReverted; | ||
| // ND: so this rule only check that the last added one can be fetched, right? |
There was a problem hiding this comment.
Yes: once a module is added, the system cannot be "stuck".
2 participants
No description provided.