NoBey/openzeppelin-contracts
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

fix spec file

Browse Source
This commit is contained in:
Hadrien Croubois
2023-05-09 10:31:17 +02:00
parent e9779f8ef2
commit 2e1d0b3756
1 changed files with 3 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
certora/specs/GovernorStates.spec
View File

@ -5,8 +5,8 @@ import "GovernorInvariants.spec"
use invariant proposalStateConsistency use invariant proposalStateConsistency
use invariant votesImplySnapshotPassed use invariant votesImplySnapshotPassed
definition assumedSafeOrDuplicateOrDuplicate(method f) returns bool = definition assumedSafeOrDuplicate(method f) returns bool =
assumedSafeOrDuplicate(f) assumedSafe(f)
|| f.selector == castVoteWithReason(uint256,uint8,string).selector || f.selector == castVoteWithReason(uint256,uint8,string).selector
|| f.selector == castVoteWithReasonAndParams(uint256,uint8,string,bytes).selector || f.selector == castVoteWithReasonAndParams(uint256,uint8,string,bytes).selector
|| f.selector == castVoteBySig(uint256,uint8,uint8,bytes32,bytes32).selector || f.selector == castVoteBySig(uint256,uint8,uint8,bytes32,bytes32).selector
@ -19,7 +19,7 @@ definition assumedSafeOrDuplicateOrDuplicate(method f) returns bool =
*/ */
invariant stateConsistency(env e, uint256 pId) invariant stateConsistency(env e, uint256 pId)
state(e, pId) == safeState(e, pId) state(e, pId) == safeState(e, pId)
filtered { f -> !assumedSafeOrDuplicateOrDuplicate(f); } filtered { f -> !assumedSafeOrDuplicate(f) }
rule stateDomain(env e, uint256 pId) { rule stateDomain(env e, uint256 pId) {
uint8 result = safeState(e, pId); uint8 result = safeState(e, pId);