From 9f2d511d20991568e28fea9cb384b03a3231ad96 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Mon, 27 Feb 2023 14:01:59 +0100 Subject: [PATCH] fix2 --- certora/applyHarness.patch | 4 ++-- certora/harnesses/GovernorFullHarness.sol | 12 +++++------- 2 files changed, 7 insertions(+), 9 deletions(-) diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch index b9f95e0c8..b073cad96 100644 --- a/certora/applyHarness.patch +++ b/certora/applyHarness.patch @@ -84,7 +84,7 @@ diff -druN governance/TimelockController.sol governance/TimelockController.sol * @dev Emitted when a call is scheduled as part of operation `id`. diff -druN governance/utils/Votes.sol governance/utils/Votes.sol --- governance/utils/Votes.sol 2023-02-27 10:59:32.655891529 +0100 -+++ governance/utils/Votes.sol 2023-02-27 13:45:38.363620120 +0100 ++++ governance/utils/Votes.sol 2023-02-27 13:56:39.610815192 +0100 @@ -35,7 +35,25 @@ bytes32 private constant _DELEGATION_TYPEHASH = keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)"); @@ -102,7 +102,7 @@ diff -druN governance/utils/Votes.sol governance/utils/Votes.sol + return SafeCast.toUint32(_delegateCheckpoints[account]._checkpoints.length); + } + function ckptFromBlock(address account, uint32 pos) public view returns (uint32) { -+ return _delegateCheckpoints[account]._checkpoints[pos]._blockNumber; ++ return _delegateCheckpoints[account]._checkpoints[pos]._key; + } + function ckptVotes(address account, uint32 pos) public view returns (uint224) { + return _delegateCheckpoints[account]._checkpoints[pos]._value; diff --git a/certora/harnesses/GovernorFullHarness.sol b/certora/harnesses/GovernorFullHarness.sol index c4ce83959..bb59ae57f 100644 --- a/certora/harnesses/GovernorFullHarness.sol +++ b/certora/harnesses/GovernorFullHarness.sol @@ -17,9 +17,7 @@ contract GovernorFullHarness is GovernorVotes, GovernorVotesQuorumFraction { - using SafeCast for uint256; - using Timers for Timers.BlockNumber; - using Checkpoints for Checkpoints.History; + using Checkpoints for Checkpoints.Trace224; constructor( IVotes _token, @@ -38,7 +36,7 @@ contract GovernorFullHarness is // variable added to check when _castVote is called uint256 public latestCastVoteCall; - + // Harness from Votes // function getPastTotalSupply(uint256 blockNumber) public view returns(uint256) { @@ -65,15 +63,15 @@ contract GovernorFullHarness is } function getExtendedDeadlineIsUnset(uint256 proposalId) public view returns (bool) { - return _extendedDeadlines[proposalId].isUnset(); + return _extendedDeadlines[proposalId] == 0; } function getExtendedDeadlineIsStarted(uint256 proposalId) public view returns (bool) { - return _extendedDeadlines[proposalId].isStarted(); + return _extendedDeadlines[proposalId] > 0; } function getExtendedDeadline(uint256 proposalId) public view returns (uint64) { - return _extendedDeadlines[proposalId].getDeadline(); + return _extendedDeadlines[proposalId]; } // Harness from GovernorCountingSimple //