From fdc4b0cf239df941aaf5fb8ebdad5c6c8981a2c9 Mon Sep 17 00:00:00 2001
From: Shelly Grossman <shelly@certora.com>
Date: Sun, 26 Sep 2021 01:39:27 +0300
Subject: [PATCH] fixes

---
 certora/specs/GovernorBase.spec | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec
index 85c20162b..99c712872 100644
--- a/certora/specs/GovernorBase.spec
+++ b/certora/specs/GovernorBase.spec
@@ -2,6 +2,7 @@
 methods {
     proposalSnapshot(uint256) returns uint256 envfree // matches proposalVoteStart
 }
+
 ghost proposalVoteStart(uint256) returns uint64 {
     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);
 }
 
-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 (
-        proposalVoteStart@new(pId) == newValue
+        proposalVoteStart@new(pId) == newValue & (max_uint64-1)
         && (forall uint256 pId2. pId != pId2 => proposalVoteStart@new(pId2) == proposalVoteStart@old(pId2))
     );
 }
 
-hook Sload uint64 value _proposals[KEY uint256 pId].(offset 0).(offset 0) STORAGE {
-    require proposalVoteStart(pId) == value;
+hook Sload uint64 value _proposals[KEY uint256 pId] STORAGE {
+    require proposalVoteStart(pId) == value & (max_uint64-1);
 }
 
 
 hook Sstore _proposals[KEY uint256 pId].(offset 32).(offset 0) uint64 newValue STORAGE {
     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))
     );
 }
 
 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) {