Conversation
…rner Feat: simplified burner
…upgrade-tests-access-control test: hash consensus: add access control tests
Removed inline-assembly, MemUtils tests Updated applyHarness Fixed Beacon chain depositor munged
…s-tests Feature/nor limits tests
| uint256 slotsPerEpoch; uint256 secondsPerSlot; uint256 genesisTime; | ||
| slotsPerEpoch, secondsPerSlot, genesisTime = getChainConfig(e); | ||
|
|
||
| assert (epochsPerFrame2 >= epochsPerFrame1) => |
There was a problem hiding this comment.
Better using the actual implementation of the slot calculation rather than copying it here.
| env e; calldataarg args; env e2; env e3; | ||
|
|
||
| submitReportData(e,args); | ||
| submitReportExtraDataEmpty(e2); |
There was a problem hiding this comment.
Correct me If I'm wrong, but this rule can be generalized for any method in-between: no matter what happens between the two submissions, one cannot submit the same report twice (since it represents the same ref slot).
There was a problem hiding this comment.
Yes, you are correct. I am adding a parametric rule to check the "any method called" case, which is more general than the current rule. Thanks.
| env e; calldataarg args; env e2; calldataarg args2; env e3; | ||
|
|
||
| submitReportData(e,args); | ||
| submitReportExtraDataList(e2,args2); |
There was a problem hiding this comment.
Same here, for cannotSubmitSameReportAfterSubmitExtraDataEmpty().
| // } | ||
|
|
||
| definition UINT64_MAX() returns uint64 = 0xFFFFFFFFFFFFFFFF; | ||
| definition UINT256_MAX() returns uint256 = 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff; |
There was a problem hiding this comment.
FYI, this is defined in CVL as 'max_uint'.
| * Methods Declaration * | ||
| **************************************************/ | ||
| methods { | ||
| submitConsensusReport(bytes32 report, uint256 refSlot, uint256 deadline) => NONDET |
There was a problem hiding this comment.
That's a state changing method, why not dispatch?
There was a problem hiding this comment.
The only state variable changed by this call is in the called contract, i.e., BaseOracle.
Also, HashConsensus is not using this state variable.
So from the HashConsensus.sol point of view, it doesn't matter.
| // definition MANAGE_CONSENSUS_CONTRACT_ROLE() returns bytes32 = 0x04a0afbbd09d5ad397fc858789da4f8edd59f5ca5098d70faa490babee945c3b; //keccak256("MANAGE_CONSENSUS_CONTRACT_ROLE"); | ||
| // definition MANAGE_CONSENSUS_VERSION_ROLE() returns bytes32 = 0xc31b1e4b732c5173dc51d519dfa432bad95550ecc4b0f9a61c2a558a2a8e4341; //keccak256("MANAGE_CONSENSUS_VERSION_ROLE"); | ||
| // definition SUBMIT_DATA_ROLE() returns bytes32 = 0x65fa0c17458517c727737e4153dd477fa3e328cf706640b0f68b1a285c5990da; //keccak256("SUBMIT_DATA_ROLE"); | ||
| definition UNREACHABLE_QUORUM() returns uint256 = max_uint256; // type(uint256).max |
| require epochsPerFrame < 31536000; // assuming less than 1 year per frame | ||
|
|
||
| // assuming correct configuration of the frame, otherwise revert | ||
| require initialEpoch < (e.block.timestamp - genesisTime) / (secondsPerSlot * slotsPerEpoch); |
There was a problem hiding this comment.
Can it be proved as an invariant, given that every call is at timestamp > genesis?
| /************************************************** | ||
| * CVL FUNCS & DEFS * | ||
| **************************************************/ | ||
| function saneTimeConfig() { |
There was a problem hiding this comment.
Why do you declare the env variable inside the function, and not use it as an input variable?
| 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.
While this is a reasonable assumption, you must add it to the report.
|
|
||
| uint256 initialEpoch; uint256 epochsPerFrame; uint256 fastLaneLengthSlots; | ||
| initialEpoch, epochsPerFrame, fastLaneLengthSlots = getFrameConfig(e0); | ||
| require epochsPerFrame > 0; // constructor already ensures this |
There was a problem hiding this comment.
Can we write an invariant that verifies their non-zero value?
| require epochsPerFrame < 31536000; // assuming less than 1 year per frame | ||
|
|
||
| // assuming correct configuration of the frame, otherwise revert | ||
| require initialEpoch < (e0.block.timestamp - genesisTime) / (secondsPerSlot * slotsPerEpoch); |
There was a problem hiding this comment.
Same here. I guess it relies on the constructor?
Might it be changed during the contract's lifecycle?
| // especially getCurrentFrame() as it is used by LegacyOracle and BaseOracle | ||
| // Status: Fail | ||
| // https://vaas-stg.certora.com/output/80942/985192ce8baf4725a8b6d29c1d0dc2af/?anonymousKey=f2574e5803ece9f5b8d734ecd68b1d9ac714c1d5 | ||
| rule viewFunctionsDoNotRevert(method f) |
There was a problem hiding this comment.
I suppose that if you intend verifying this rule, you want to include the sane assumptions block you've created?
14 participants
No description provided.