From f239fa56dd35c7b5b52303646311c07dcef15117 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Sun, 26 Sep 2021 00:25:59 +0300 Subject: [PATCH] Back to expected pattern? --- certora/specs/GovernorBase.spec | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec index 58c07582f..85c20162b 100644 --- a/certora/specs/GovernorBase.spec +++ b/certora/specs/GovernorBase.spec @@ -15,14 +15,14 @@ ghost proposalCanceled(uint256) returns bool { init_state axiom forall uint256 pId. !proposalCanceled(pId); } -hook Sstore _proposals[KEY uint256 pId].(offset 0) uint64 newValue STORAGE { +hook Sstore _proposals[KEY uint256 pId].(offset 0).(offset 0) uint64 newValue STORAGE { havoc proposalVoteStart assuming ( proposalVoteStart@new(pId) == newValue && (forall uint256 pId2. pId != pId2 => proposalVoteStart@new(pId2) == proposalVoteStart@old(pId2)) ); } -hook Sload uint64 value _proposals[KEY uint256 pId].(offset 0) STORAGE { +hook Sload uint64 value _proposals[KEY uint256 pId].(offset 0).(offset 0) STORAGE { require proposalVoteStart(pId) == value; }