Shelly Grossman 4 years ago
parent
commit
a0cb8cd446
1 changed files with 6 additions and 4 deletions
  1. 6 4
      certora/specs/GovernorBase.spec

+ 6 - 4
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) {