Back to expected pattern?

pull/2997/head
Shelly Grossman 3 years ago
parent 2c08f85744
commit f239fa56dd
  1. 4
      certora/specs/GovernorBase.spec

@ -15,14 +15,14 @@ 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) uint64 newValue STORAGE { hook Sstore _proposals[KEY uint256 pId].(offset 0).(offset 0) uint64 newValue STORAGE {
havoc proposalVoteStart assuming ( havoc proposalVoteStart assuming (
proposalVoteStart@new(pId) == newValue proposalVoteStart@new(pId) == newValue
&& (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) STORAGE { hook Sload uint64 value _proposals[KEY uint256 pId].(offset 0).(offset 0) STORAGE {
require proposalVoteStart(pId) == value; require proposalVoteStart(pId) == value;
} }

Loading…
Cancel
Save