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

fixes

Browse Source
This commit is contained in:
Shelly Grossman
2021-09-26 01:39:27 +03:00
parent f239fa56dd
commit fdc4b0cf23
1 changed files with 7 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files

13
certora/specs/GovernorBase.spec
View File

@ -2,6 +2,7 @@
methods { methods {
proposalSnapshot(uint256) returns uint256 envfree // matches proposalVoteStart proposalSnapshot(uint256) returns uint256 envfree // matches proposalVoteStart
} }
ghost proposalVoteStart(uint256) returns uint64 { ghost proposalVoteStart(uint256) returns uint64 {
init_state axiom forall uint256 pId. proposalVoteStart(pId) == 0; init_state axiom forall uint256 pId. proposalVoteStart(pId) == 0;
} }
@ -15,27 +16,27 @@ ghost proposalCanceled(uint256) returns bool {
init_state axiom forall uint256 pId. !proposalCanceled(pId); init_state axiom forall uint256 pId. !proposalCanceled(pId);
} }
hook Sstore _proposals[KEY uint256 pId].(offset 0).(offset 0) uint64 newValue STORAGE { hook Sstore _proposals[KEY uint256 pId] uint64 newValue STORAGE {
havoc proposalVoteStart assuming ( havoc proposalVoteStart assuming (
proposalVoteStart@new(pId) == newValue proposalVoteStart@new(pId) == newValue & (max_uint64-1)
&& (forall uint256 pId2. pId != pId2 => proposalVoteStart@new(pId2) == proposalVoteStart@old(pId2)) && (forall uint256 pId2. pId != pId2 => proposalVoteStart@new(pId2) == proposalVoteStart@old(pId2))
); );
} }
hook Sload uint64 value _proposals[KEY uint256 pId].(offset 0).(offset 0) STORAGE { hook Sload uint64 value _proposals[KEY uint256 pId] STORAGE {
require proposalVoteStart(pId) == value; require proposalVoteStart(pId) == value & (max_uint64-1);
} }
hook Sstore _proposals[KEY uint256 pId].(offset 32).(offset 0) uint64 newValue STORAGE { hook Sstore _proposals[KEY uint256 pId].(offset 32).(offset 0) uint64 newValue STORAGE {
havoc proposalVoteEnd assuming ( havoc proposalVoteEnd assuming (
proposalVoteEnd@new(pId) == newValue proposalVoteEnd@new(pId) == newValue & (max_uint64-1)
&& (forall uint256 pId2. pId != pId2 => proposalVoteEnd@new(pId2) == proposalVoteEnd@old(pId2)) && (forall uint256 pId2. pId != pId2 => proposalVoteEnd@new(pId2) == proposalVoteEnd@old(pId2))
); );
} }
hook Sload uint64 value _proposals[KEY uint256 pId].(offset 32).(offset 0) STORAGE { hook Sload uint64 value _proposals[KEY uint256 pId].(offset 32).(offset 0) STORAGE {
require proposalVoteEnd(pId) == value; require proposalVoteEnd(pId) == value & (max_uint64-1);
} }
rule sanityCheckVoteStart(method f, uint256 pId) { rule sanityCheckVoteStart(method f, uint256 pId) {