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

executedImplyStartAndEndDateNonZero inv fix

Browse Source
This commit is contained in:
Aleksander Kryukov
2021-11-25 16:25:40 +02:00
parent 1d25a22201
commit 43e37f0184
1 changed files with 4 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files

7
certora/specs/GovernorBase.spec
View File

@ -98,9 +98,9 @@ function helperFunctionsWithRevert(uint256 proposalId, method f, env e) {
// To use env with general preserved block disable type checking [--disableLocalTypeChecking] // To use env with general preserved block disable type checking [--disableLocalTypeChecking]
invariant startAndEndDatesNonZero(uint256 pId) invariant startAndEndDatesNonZero(uint256 pId)
proposalSnapshot(pId) != 0 <=> proposalDeadline(pId) != 0 proposalSnapshot(pId) != 0 <=> proposalDeadline(pId) != 0
/*{ preserved with (env e){ { preserved with (env e){
require e.block.number > 0; require e.block.number > 0;
}}*/ }}
/* /*
@ -121,7 +121,8 @@ invariant canceledImplyStartAndEndDateNonZero(uint pId)
invariant executedImplyStartAndEndDateNonZero(uint pId) invariant executedImplyStartAndEndDateNonZero(uint pId)
isExecuted(pId) => proposalSnapshot(pId) != 0 isExecuted(pId) => proposalSnapshot(pId) != 0
{ preserved with (env e){ { preserved with (env e){
require e.block.number > 0; requireInvariant startAndEndDatesNonZero(pId);
require e.block.number > 0;
}} }}