formal-verification
Hadrien Croubois 2 years ago
parent b50d9980be
commit 9f2d511d20
  1. 4
      certora/applyHarness.patch
  2. 12
      certora/harnesses/GovernorFullHarness.sol

@ -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;

@ -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 //

Loading…
Cancel
Save