diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec index 99c712872..32b0fd21b 100644 --- a/certora/specs/GovernorBase.spec +++ b/certora/specs/GovernorBase.spec @@ -16,27 +16,29 @@ ghost proposalCanceled(uint256) returns bool { init_state axiom forall uint256 pId. !proposalCanceled(pId); } +definition mask_uint64() returns uint256 = max_uint64 - 1; + hook Sstore _proposals[KEY uint256 pId] uint64 newValue STORAGE { havoc proposalVoteStart assuming ( - proposalVoteStart@new(pId) == newValue & (max_uint64-1) + proposalVoteStart@new(pId) == newValue & mask_uint64() && (forall uint256 pId2. pId != pId2 => proposalVoteStart@new(pId2) == proposalVoteStart@old(pId2)) ); } hook Sload uint64 value _proposals[KEY uint256 pId] STORAGE { - require proposalVoteStart(pId) == value & (max_uint64-1); + require proposalVoteStart(pId) == value & mask_uint64(); } hook Sstore _proposals[KEY uint256 pId].(offset 32).(offset 0) uint64 newValue STORAGE { havoc proposalVoteEnd assuming ( - proposalVoteEnd@new(pId) == newValue & (max_uint64-1) + proposalVoteEnd@new(pId) == newValue & mask_uint64() && (forall uint256 pId2. pId != pId2 => proposalVoteEnd@new(pId2) == proposalVoteEnd@old(pId2)) ); } hook Sload uint64 value _proposals[KEY uint256 pId].(offset 32).(offset 0) STORAGE { - require proposalVoteEnd(pId) == value & (max_uint64-1); + require proposalVoteEnd(pId) == value & mask_uint64(); } rule sanityCheckVoteStart(method f, uint256 pId) {