Hristo/hash-consensus PR for spec review#22
Hristo/hash-consensus PR for spec review#22hristo-grigorov wants to merge 15 commits intofeature/shapella-upgradefrom
Conversation
hristo-grigorov
requested review from
DanieLion55,
GadElbazCertora,
RedLikeRosesss,
Roy-Certora and
tomerganor
|
|
||
| address prevAddr = CONSENSUS_CONTRACT_POSITION.getStorageAddress(); | ||
| if (addr == prevAddr) revert AddressCannotBeSame(); | ||
| //if (addr == prevAddr) revert AddressCannotBeSame(); // Certora munging: commented out |
There was a problem hiding this comment.
This is for the AccountingOracle verification. There I am forcing the address of the Consensus contract to be the one I explicitly add to the scene (using require). And because of that requirement, any time a call to the function that changes the address of the consensus contract is done, I get reachability issues.
| } | ||
|
|
||
| // A helper function to get event info of successful report submit | ||
| function getSuccessfulReportSubmitEventInfo(uint256 refSlot, address member, bytes32 report) returns uint256 { |
There was a problem hiding this comment.
This is the trigger summarization of the emit event you've created.
What happens if this trigger is called twice with different arguments?
Your require statements for the ghosts will enforce the arguments to be same (or vacuity).
There was a problem hiding this comment.
In general, only if a report was submitted successfully two times in a row and I need to check this case, will it matter. But I don't have such a rule or check so I believe the current use is OK.
| } | ||
|
|
||
| // focus only on getCurrentFrame() and verify it does not revert | ||
| // Status: Timeout! (without the simplification, shown in saneTimeConfig()) |
There was a problem hiding this comment.
You could have increased the time out settings even more, but the simplification is OK I guess.
| !hasRole_DISABLE_CONSENSUS_ROLE) => (quorumBefore == quorumAfter); // cannot change the quorum | ||
|
|
||
| assert ((f.selector == disableConsensus().selector) && | ||
| quorumBefore != UNREACHABLE_QUORUM() && // this ensures the quorum was not disabled already |
There was a problem hiding this comment.
I would expect that the call will revert regardless of the quorum state before, as only the role member can perform the transaction.
There was a problem hiding this comment.
I also thought this way, but they have a weird implementation here. They don't check the required role until a change is about to be made.
So, effectively, anyone can call the function if it does not change the state.
certora/specs/HashConsensus.spec
Outdated
| initialEpoch2, epochsPerFrame2, fastLaneLengthSlots2 = getFrameConfig(e2); | ||
|
|
||
| // verify getter returns updated values | ||
| assert epochsPerFrame == epochsPerFrame2; // only those asserts cause timeout |
There was a problem hiding this comment.
Really? Even with your saneTimeConfig?
certora/specs/HashConsensus.spec
Outdated
| uint256 slotsPerEpoch; uint256 secondsPerSlot; uint256 genesisTime; | ||
| slotsPerEpoch, secondsPerSlot, genesisTime = getChainConfig(e2); | ||
|
|
||
| assert refSlot2 >= refSlot1; // fails |
There was a problem hiding this comment.
Do we understand why?
Is it a bug?
| // Status: Pass | ||
| // https://prover.certora.com/output/80942/d9d92700466f42b9b284bb7c0664314e/?anonymousKey=dfbcd43aa6f2a327b2fbe32e2ed4b51a06f52f3e | ||
| rule addMemberRevertsCorrectly() { | ||
| env e; env e2; |
|
|
||
| require userA != userB; // userA and userB are different | ||
|
|
||
| assert isUserBMemberBefore => isUserBMemberAfter; // adding userA does not remove userB |
There was a problem hiding this comment.
Maybe I didn't understand your intention, but it seems that fetching the member state of userA is not needed, and these two asserts could be combined into one with double implication (<=>).
| uint256 lengthOf_memberAddressesBefore; uint256 lengthOf_memberStatesBefore; | ||
| lengthOf_memberAddressesBefore, lengthOf_memberStatesBefore = getLengthOfArrays(e); // using helper | ||
|
|
||
| require lengthOf_memberAddressesBefore == lengthOf_memberStatesBefore; // those arrays represent the same members |
There was a problem hiding this comment.
Seems like a reasonable assumption, but can you prove it?
| // 15. submitReport() - slot > max_uint64 => revert | ||
| // Status: Pass | ||
| // https://prover.certora.com/output/80942/870be390cf09430f8177e17e1f2d685c/?anonymousKey=bd2021b839df527ae29aa419b43d14beb25c87ea | ||
| rule cannotSubmitReportWhenSlotIsAboveMaxUint64() { |
There was a problem hiding this comment.
Is there a stronger claim we could make about the maximal value of the slot for the function to not revert?
max_uint64 is pretty trivial.
| uint256 lastProcessingRefSlot = helper_getLastProcessingRefSlot(e); | ||
|
|
||
| uint256 slot; bytes32 report; uint256 consensusVersion; | ||
| require slot > lastProcessingRefSlot; // otherwise the report doesn't matter |
There was a problem hiding this comment.
Doesn't it mean that the first call would revert for a slot <= lastSlot?
I wonder if the require is needed at all...
| // | ||
|
|
||
|
|
||
| // 23. submitReport() - when new frame starts _reportVariantsLength should reset to 1 |
There was a problem hiding this comment.
I don't understand the implementation of this rule.
Why doesn't it look like:
frame_after != frame_before => length == 1
| // https://prover.certora.com/output/80942/5c86836015fc4c9baa0cb035e635975a/?anonymousKey=86dce987e054b75ffa9e119ff360e6a47d607156 | ||
| rule updateInitialEpochRevertsCorrectly() { | ||
| env e; calldataarg args; | ||
| require e.block.timestamp > saneTimeConfig(); // time moves forward (saneTimeConfig is for correct initializing) |
There was a problem hiding this comment.
Is there a lighter restriction that will verify this rule?
It's not really necessary to assume everything here, right?
| uint256 initialEpoch; uint256 epochsPerFrame; uint256 fastLaneLengthSlots; | ||
| initialEpoch, epochsPerFrame, fastLaneLengthSlots = getFrameConfig(e2); | ||
|
|
||
| assert initialEpoch <= ((e2.block.timestamp - genesisTime) / (secondsPerSlot * slotsPerEpoch)); // sane configuration of initialEpoch |
There was a problem hiding this comment.
Can you replace the calculation with the actual function call?
|
|
||
| uint256 slotsPerEpoch; uint256 secondsPerSlot; uint256 genesisTime; | ||
| slotsPerEpoch, secondsPerSlot, genesisTime = getChainConfig(e0); | ||
| require slotsPerEpoch == 32; // simplification, must be required at constructor |
There was a problem hiding this comment.
What happens if you replace all effective assignments like this one, to range restrictions.
e.g. require 100 >= slotsPerEpoch > 0
| // verify with getFrameConfig() | ||
| // Status: Pass | ||
| // https://prover.certora.com/output/80942/133f5763d704400b8bf17e08db8d01d6/?anonymousKey=c467fc94b9572fb48f8790f6c5ba5872f188ea1b | ||
| rule setFastLaneLengthSlotsCorrectness() { |
There was a problem hiding this comment.
This seems like a particular case of a more general integrity rule, where instead of zero there could have been an arbitrary value.
Why is this case interesting?
| } | ||
|
|
||
|
|
||
| // 20. submitReport() - verify that the deadline (frame.reportProcessingDeadlineSlot) is explicitly == refSlot + FrameSize |
There was a problem hiding this comment.
Examining the counter example, I think you need to add some requirement on the maximum value of the refSlot, it looks too big.
| bool isUserAMemberAfter = getIsMember(e2,userA); | ||
|
|
||
| assert !isUserAMemberBefore; // cannot add userA if he was a member before | ||
| assert isUserAMemberAfter; // adding userA correctly |
There was a problem hiding this comment.
you call addMember(), so it implies that userA wasn't a member and will be a member after because there is no @withrevert. Does it make sense to add these asserts?
| uint256 lengthOf_memberAddressesBefore; uint256 lengthOf_memberStatesBefore; | ||
| lengthOf_memberAddressesBefore, lengthOf_memberStatesBefore = getLengthOfArrays(e); // using helper | ||
|
|
||
| if (!isUserBMemberBefore) { |
| rule removeMemberADoesNotModifyMemberB() { | ||
| env e; env e2; | ||
| address userA; uint256 quorum; address userB; | ||
| bool isUserAMemberBefore = getIsMember(e,userA); |
There was a problem hiding this comment.
seems like getters for userA are not used, maybe remove it to make code cleaner?
| lengthOf_memberAddressesAfter, lengthOf_memberStatesAfter = getLengthOfArrays(e); // using helper | ||
| bool isUserAMemberAfter = getIsMember(e2,userA); | ||
|
|
||
| assert isUserAMemberBefore; // cannot remove userA if he was not a member before |
There was a problem hiding this comment.
it seems the same as with addMember(). You call removeMember() without @withrevert, so this asserts are guaranteed
| bytes32 report2; | ||
| submitReport@withrevert(e2, slot, report2, consensusVersion); | ||
|
|
||
| assert (ghostReportHash != 0) && (e2.msg.sender == e.msg.sender) && (report != report2) => lastReverted; |
There was a problem hiding this comment.
do you need (ghostReportHash != 0)? if it revert with the same sender and report, then it will revert
3 participants
This Draft PR includes the HashConsensus and AccountingOracle specs and code munging.