setup for day1 #13
setup for day1 #13
Conversation
There was a problem hiding this comment.
Looks good. I left some minor comments.
I already started to work on the examples as well. Here's my code https://github.com/Certora/liquid-collective-protocol/blob/otakar/training/certora/specs/OperatorRegistryV1.spec
I like your rules better but maybe this can still help. There's also a parametric rule for day 2.
There was a problem hiding this comment.
Most of the harness methods are not needed for the training.
There was a problem hiding this comment.
yes, but I think they are not confusing. I did change the returned type of getOperatorState , do you think it is good? maybe need to adopt your spec as well?
certora/specs/OperatorRegistry.spec
Outdated
| uint32 limitAfter; | ||
| _, limitAfter, _, _, _, _, _ = getOperatorState(e, opIndex); |
There was a problem hiding this comment.
There's an easier way to write this.
uint32 limitAfter = getOperator(opIndex).limit;
|
|
||
| uint32 limitAfter; | ||
| _, limitAfter, _, _, _, _, _ = getOperatorState(opIndex); | ||
| satisfy limitAfter == limitBefore; |
There was a problem hiding this comment.
This can be satisfied by choosing newLimits[i] = limitBefore, right? Is that what we want to show?
A witness for changing the variable would make more sense to me. I.e. satisfy limitAfter != limitBefore to show that rule integritySetOperatorLimits is not vacuous.
There was a problem hiding this comment.
exactly, I want us to try many cases, and also notice when we want the separate satisfy
certora/specs/OperatorRegistry.spec
Outdated
| uint32 limitBefore; | ||
| uint256 latestKeysEditBlockNumber; | ||
|
|
||
| _, limitBefore, _, _, _, _, _ = getOperatorState(opIndex); |
There was a problem hiding this comment.
Can be simplified via getOperator(opIndex).limit
certora/specs/OperatorRegistry.spec
Outdated
| uint256 latestKeysEditBlockNumber; | ||
|
|
||
| _, limitBefore, _, _, _, _, _ = getOperatorState(opIndex); | ||
| latestKeysEditBlockNumber = getLatestKeysEditBlockNumber(opIndex); |
There was a problem hiding this comment.
This can also be simplified as getOperator(opIndex).latestKeysEditBlockNumber - without the need for a harness method, but this looks fine too.
Also the variable latestKeysEditBlockNumber is never used but I guess you plan to use it during the lesson somehow.
|
|
||
| import "../../contracts/src/OperatorsRegistry.1.sol"; | ||
| import "../../contracts/src/state/operatorsRegistry/Operators.2.sol"; | ||
| contract OperatorsRegistryV1Harness is OperatorsRegistryV1 { |
There was a problem hiding this comment.
I think we should only keep the methods we need in the harness.
|
|
||
| /** | ||
| @title - integrity of a successful (non reverting) to setOperatorLimits() | ||
| // todo - violated, undersntad why and fix |
Shoham/training
Signed-off-by: Otakar Trunda <114909958+otakar-trunda@users.noreply.github.com>
…e-protocol into certoraTraining
Description
Notice
Pull Request Type
Breaking changes (if applicable)
Testing
Manual tests (if applicable)
Additional comments