mirror
/
openzeppelin-contracts
mirror of https://github.com/OpenZeppelin/openzeppelin-contracts
2
1
Fork 1
Code Issues Releases Wiki Activity

votes solvency passing again

Browse Source
pull/3480/head
Nick Armstrong 3 years ago
parent 4820ed4ea8
commit 2627753bfe
3 changed files with 101 additions and 72 deletions
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Show Stats Download Patch File Download Diff File
  1. 143
      certora/applyHarness.patch
  2. 5
      certora/scripts/Round2/verifyERC20Votes.sh
  3. 21
      certora/specs/ERC20Votes.spec

143
certora/applyHarness.patch
Unescape View File

@ -1,12 +1,12 @@
diff -ruN .gitignore .gitignore
--- .gitignore 1969-12-31 16:00:00.000000000 -0800
+++ .gitignore 2022-08-11 21:15:52.000000000 -0700
+++ .gitignore 2022-08-11 21:28:36.000000000 -0700
@@ -0,0 +1,2 @@
+*
+!.gitignore
diff -ruN access/AccessControl.sol access/AccessControl.sol
--- access/AccessControl.sol 2022-08-11 21:13:55.000000000 -0700
+++ access/AccessControl.sol 2022-08-11 21:15:52.000000000 -0700
--- access/AccessControl.sol 2022-08-11 21:28:00.000000000 -0700
+++ access/AccessControl.sol 2022-08-11 21:28:36.000000000 -0700
@@ -93,7 +93,7 @@
*
* _Available since v4.6._
@ -17,8 +17,8 @@ diff -ruN access/AccessControl.sol access/AccessControl.sol
}
diff -ruN access/Ownable.sol access/Ownable.sol
--- access/Ownable.sol 2022-08-11 21:13:55.000000000 -0700
+++ access/Ownable.sol 2022-08-11 21:15:52.000000000 -0700
--- access/Ownable.sol 2022-08-11 21:28:00.000000000 -0700
+++ access/Ownable.sol 2022-08-11 21:28:36.000000000 -0700
@@ -30,14 +30,6 @@
}
@ -49,8 +49,8 @@ diff -ruN access/Ownable.sol access/Ownable.sol
/**
diff -ruN governance/Governor.sol governance/Governor.sol
--- governance/Governor.sol 2022-08-11 21:13:55.000000000 -0700
+++ governance/Governor.sol 2022-08-11 21:15:52.000000000 -0700
--- governance/Governor.sol 2022-08-11 21:28:00.000000000 -0700
+++ governance/Governor.sol 2022-08-11 21:28:36.000000000 -0700
@@ -44,7 +44,7 @@
string private _name;
@ -61,8 +61,8 @@ diff -ruN governance/Governor.sol governance/Governor.sol
// This queue keeps track of the governor operating on itself. Calls to functions protected by the
// {onlyGovernance} modifier needs to be whitelisted in this queue. Whitelisting is set in {_beforeExecute},
diff -ruN governance/TimelockController.sol governance/TimelockController.sol
--- governance/TimelockController.sol 2022-08-11 21:13:55.000000000 -0700
+++ governance/TimelockController.sol 2022-08-11 21:15:52.000000000 -0700
--- governance/TimelockController.sol 2022-08-11 21:28:00.000000000 -0700
+++ governance/TimelockController.sol 2022-08-11 21:28:36.000000000 -0700
@@ -28,10 +28,10 @@
bytes32 public constant PROPOSER_ROLE = keccak256("PROPOSER_ROLE");
bytes32 public constant EXECUTOR_ROLE = keccak256("EXECUTOR_ROLE");
@ -77,8 +77,8 @@ diff -ruN governance/TimelockController.sol governance/TimelockController.sol
/**
* @dev Emitted when a call is scheduled as part of operation `id`.
diff -ruN governance/extensions/GovernorCountingSimple.sol governance/extensions/GovernorCountingSimple.sol
--- governance/extensions/GovernorCountingSimple.sol 2022-08-11 21:13:55.000000000 -0700
+++ governance/extensions/GovernorCountingSimple.sol 2022-08-11 21:15:52.000000000 -0700
--- governance/extensions/GovernorCountingSimple.sol 2022-08-11 21:28:00.000000000 -0700
+++ governance/extensions/GovernorCountingSimple.sol 2022-08-11 21:28:36.000000000 -0700
@@ -27,7 +27,7 @@
mapping(address => bool) hasVoted;
}
@ -89,8 +89,8 @@ diff -ruN governance/extensions/GovernorCountingSimple.sol governance/extensions
/**
* @dev See {IGovernor-COUNTING_MODE}.
diff -ruN governance/extensions/GovernorPreventLateQuorum.sol governance/extensions/GovernorPreventLateQuorum.sol
--- governance/extensions/GovernorPreventLateQuorum.sol 2022-08-11 21:13:55.000000000 -0700
+++ governance/extensions/GovernorPreventLateQuorum.sol 2022-08-11 21:15:52.000000000 -0700
--- governance/extensions/GovernorPreventLateQuorum.sol 2022-08-11 21:28:00.000000000 -0700
+++ governance/extensions/GovernorPreventLateQuorum.sol 2022-08-11 21:28:36.000000000 -0700
@@ -21,8 +21,8 @@
using SafeCast for uint256;
using Timers for Timers.BlockNumber;
@ -103,8 +103,8 @@ diff -ruN governance/extensions/GovernorPreventLateQuorum.sol governance/extensi
/// @dev Emitted when a proposal deadline is pushed back due to reaching quorum late in its voting period.
event ProposalExtended(uint256 indexed proposalId, uint64 extendedDeadline);
diff -ruN governance/utils/Votes.sol governance/utils/Votes.sol
--- governance/utils/Votes.sol 2022-08-11 21:13:55.000000000 -0700
+++ governance/utils/Votes.sol 2022-08-11 21:15:52.000000000 -0700
--- governance/utils/Votes.sol 2022-08-11 21:28:00.000000000 -0700
+++ governance/utils/Votes.sol 2022-08-11 21:28:36.000000000 -0700
@@ -35,7 +35,25 @@
bytes32 private constant _DELEGATION_TYPEHASH =
keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)");
@ -178,8 +178,8 @@ diff -ruN governance/utils/Votes.sol governance/utils/Votes.sol
+ function _getVotingUnits(address) public virtual returns (uint256); // HARNESS: internal -> public
}
diff -ruN metatx/MinimalForwarder.sol metatx/MinimalForwarder.sol
--- metatx/MinimalForwarder.sol 2022-08-11 21:13:55.000000000 -0700
+++ metatx/MinimalForwarder.sol 2022-08-11 21:15:52.000000000 -0700
--- metatx/MinimalForwarder.sol 2022-08-11 21:28:00.000000000 -0700
+++ metatx/MinimalForwarder.sol 2022-08-11 21:28:36.000000000 -0700
@@ -8,11 +8,6 @@
/**
@ -194,7 +194,7 @@ diff -ruN metatx/MinimalForwarder.sol metatx/MinimalForwarder.sol
using ECDSA for bytes32;
diff -ruN mocks/ERC20TokenizedVaultMock.sol mocks/ERC20TokenizedVaultMock.sol
--- mocks/ERC20TokenizedVaultMock.sol 1969-12-31 16:00:00.000000000 -0800
+++ mocks/ERC20TokenizedVaultMock.sol 2022-08-11 21:15:52.000000000 -0700
+++ mocks/ERC20TokenizedVaultMock.sol 2022-08-11 21:28:36.000000000 -0700
@@ -0,0 +1,22 @@
+// SPDX-License-Identifier: MIT
+
@ -219,7 +219,7 @@ diff -ruN mocks/ERC20TokenizedVaultMock.sol mocks/ERC20TokenizedVaultMock.sol
+ }
+}
diff -ruN mocks/ERC4626Mock.sol mocks/ERC4626Mock.sol
--- mocks/ERC4626Mock.sol 2022-08-11 21:13:55.000000000 -0700
--- mocks/ERC4626Mock.sol 2022-08-11 21:28:00.000000000 -0700
+++ mocks/ERC4626Mock.sol 1969-12-31 16:00:00.000000000 -0800
@@ -1,22 +0,0 @@
-// SPDX-License-Identifier: MIT
@ -245,8 +245,8 @@ diff -ruN mocks/ERC4626Mock.sol mocks/ERC4626Mock.sol
- }
-}
diff -ruN mocks/MathMock.sol mocks/MathMock.sol
--- mocks/MathMock.sol 2022-08-11 21:13:55.000000000 -0700
+++ mocks/MathMock.sol 2022-08-11 21:15:52.000000000 -0700
--- mocks/MathMock.sol 2022-08-11 21:28:00.000000000 -0700
+++ mocks/MathMock.sol 2022-08-11 21:28:36.000000000 -0700
@@ -29,8 +29,4 @@
) public pure returns (uint256) {
return Math.mulDiv(a, b, denominator, direction);
@ -257,8 +257,8 @@ diff -ruN mocks/MathMock.sol mocks/MathMock.sol
- }
}
diff -ruN mocks/SafeERC20Helper.sol mocks/SafeERC20Helper.sol
--- mocks/SafeERC20Helper.sol 2022-08-11 21:13:55.000000000 -0700
+++ mocks/SafeERC20Helper.sol 2022-08-11 21:15:52.000000000 -0700
--- mocks/SafeERC20Helper.sol 2022-08-11 21:28:00.000000000 -0700
+++ mocks/SafeERC20Helper.sol 2022-08-11 21:28:36.000000000 -0700
@@ -4,7 +4,6 @@
import "../utils/Context.sol";
@ -331,8 +331,8 @@ diff -ruN mocks/SafeERC20Helper.sol mocks/SafeERC20Helper.sol
ERC20ReturnTrueMock(address(_token)).setAllowance(allowance_);
}
diff -ruN proxy/Clones.sol proxy/Clones.sol
--- proxy/Clones.sol 2022-08-11 21:13:55.000000000 -0700
+++ proxy/Clones.sol 2022-08-11 21:15:52.000000000 -0700
--- proxy/Clones.sol 2022-08-11 21:28:00.000000000 -0700
+++ proxy/Clones.sol 2022-08-11 21:28:36.000000000 -0700
@@ -26,10 +26,10 @@
/// @solidity memory-safe-assembly
assembly {
@ -385,8 +385,8 @@ diff -ruN proxy/Clones.sol proxy/Clones.sol
}
diff -ruN proxy/ERC1967/ERC1967Proxy.sol proxy/ERC1967/ERC1967Proxy.sol
--- proxy/ERC1967/ERC1967Proxy.sol 2022-08-11 21:13:55.000000000 -0700
+++ proxy/ERC1967/ERC1967Proxy.sol 2022-08-11 21:15:52.000000000 -0700
--- proxy/ERC1967/ERC1967Proxy.sol 2022-08-11 21:28:00.000000000 -0700
+++ proxy/ERC1967/ERC1967Proxy.sol 2022-08-11 21:28:36.000000000 -0700
@@ -20,6 +20,7 @@
* function call, and allows initializing the storage of the proxy like a Solidity constructor.
*/
@ -396,8 +396,8 @@ diff -ruN proxy/ERC1967/ERC1967Proxy.sol proxy/ERC1967/ERC1967Proxy.sol
}
diff -ruN proxy/beacon/BeaconProxy.sol proxy/beacon/BeaconProxy.sol
--- proxy/beacon/BeaconProxy.sol 2022-08-11 21:13:55.000000000 -0700
+++ proxy/beacon/BeaconProxy.sol 2022-08-11 21:15:52.000000000 -0700
--- proxy/beacon/BeaconProxy.sol 2022-08-11 21:28:00.000000000 -0700
+++ proxy/beacon/BeaconProxy.sol 2022-08-11 21:28:36.000000000 -0700
@@ -28,6 +28,7 @@
* - `beacon` must be a contract with the interface {IBeacon}.
*/
@ -407,8 +407,8 @@ diff -ruN proxy/beacon/BeaconProxy.sol proxy/beacon/BeaconProxy.sol
}
diff -ruN proxy/transparent/TransparentUpgradeableProxy.sol proxy/transparent/TransparentUpgradeableProxy.sol
--- proxy/transparent/TransparentUpgradeableProxy.sol 2022-08-11 21:13:55.000000000 -0700
+++ proxy/transparent/TransparentUpgradeableProxy.sol 2022-08-11 21:15:52.000000000 -0700
--- proxy/transparent/TransparentUpgradeableProxy.sol 2022-08-11 21:28:00.000000000 -0700
+++ proxy/transparent/TransparentUpgradeableProxy.sol 2022-08-11 21:28:36.000000000 -0700
@@ -36,6 +36,7 @@
address admin_,
bytes memory _data
@ -418,8 +418,8 @@ diff -ruN proxy/transparent/TransparentUpgradeableProxy.sol proxy/transparent/Tr
}
diff -ruN proxy/utils/Initializable.sol proxy/utils/Initializable.sol
--- proxy/utils/Initializable.sol 2022-08-11 21:13:55.000000000 -0700
+++ proxy/utils/Initializable.sol 2022-08-11 21:15:52.000000000 -0700
--- proxy/utils/Initializable.sol 2022-08-11 21:28:00.000000000 -0700
+++ proxy/utils/Initializable.sol 2022-08-11 21:28:36.000000000 -0700
@@ -59,12 +59,12 @@
* @dev Indicates that the contract has been initialized.
* @custom:oz-retyped-from bool
@ -437,7 +437,7 @@ diff -ruN proxy/utils/Initializable.sol proxy/utils/Initializable.sol
* @dev Triggered when the contract has been initialized or reinitialized.
diff -ruN proxy/utils/Initializable.sol.orig proxy/utils/Initializable.sol.orig
--- proxy/utils/Initializable.sol.orig 1969-12-31 16:00:00.000000000 -0800
+++ proxy/utils/Initializable.sol.orig 2022-08-11 21:15:52.000000000 -0700
+++ proxy/utils/Initializable.sol.orig 2022-08-11 21:28:36.000000000 -0700
@@ -0,0 +1,138 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts (last updated v4.6.0) (proxy/utils/Initializable.sol)
@ -579,7 +579,7 @@ diff -ruN proxy/utils/Initializable.sol.orig proxy/utils/Initializable.sol.orig
+}
diff -ruN proxy/utils/Initializable.sol.rej proxy/utils/Initializable.sol.rej
--- proxy/utils/Initializable.sol.rej 1969-12-31 16:00:00.000000000 -0800
+++ proxy/utils/Initializable.sol.rej 2022-08-11 21:15:52.000000000 -0700
+++ proxy/utils/Initializable.sol.rej 2022-08-11 21:28:36.000000000 -0700
@@ -0,0 +1,17 @@
+***************
+*** 130,136 ****
@ -599,8 +599,8 @@ diff -ruN proxy/utils/Initializable.sol.rej proxy/utils/Initializable.sol.rej
+ // inheritance patterns, but we only do this in the context of a constructor, and for the lowest level
+ // of initializers, because in other contexts the contract may have been reentered.
diff -ruN security/Pausable.sol security/Pausable.sol
--- security/Pausable.sol 2022-08-11 21:13:55.000000000 -0700
+++ security/Pausable.sol 2022-08-11 21:15:52.000000000 -0700
--- security/Pausable.sol 2022-08-11 21:28:00.000000000 -0700
+++ security/Pausable.sol 2022-08-11 21:28:36.000000000 -0700
@@ -35,6 +35,13 @@
}
@ -656,8 +656,8 @@ diff -ruN security/Pausable.sol security/Pausable.sol
/**
diff -ruN token/ERC1155/ERC1155.sol token/ERC1155/ERC1155.sol
--- token/ERC1155/ERC1155.sol 2022-08-11 21:13:55.000000000 -0700
+++ token/ERC1155/ERC1155.sol 2022-08-11 21:15:52.000000000 -0700
--- token/ERC1155/ERC1155.sol 2022-08-11 21:28:00.000000000 -0700
+++ token/ERC1155/ERC1155.sol 2022-08-11 21:28:36.000000000 -0700
@@ -21,7 +21,7 @@
using Address for address;
@ -686,8 +686,8 @@ diff -ruN token/ERC1155/ERC1155.sol token/ERC1155/ERC1155.sol
try IERC1155Receiver(to).onERC1155BatchReceived(operator, from, ids, amounts, data) returns (
bytes4 response
diff -ruN token/ERC20/ERC20.sol token/ERC20/ERC20.sol
--- token/ERC20/ERC20.sol 2022-08-11 21:25:35.000000000 -0700
+++ token/ERC20/ERC20.sol 2022-08-11 21:15:52.000000000 -0700
--- token/ERC20/ERC20.sol 2022-08-11 21:28:00.000000000 -0700
+++ token/ERC20/ERC20.sol 2022-08-11 23:01:50.000000000 -0700
@@ -277,7 +277,7 @@
* - `account` cannot be the zero address.
* - `account` must have at least `amount` tokens.
@ -698,8 +698,8 @@ diff -ruN token/ERC20/ERC20.sol token/ERC20/ERC20.sol
_beforeTokenTransfer(account, address(0), amount);
diff -ruN token/ERC20/README.adoc token/ERC20/README.adoc
--- token/ERC20/README.adoc 2022-08-11 21:13:55.000000000 -0700
+++ token/ERC20/README.adoc 2022-08-11 21:15:52.000000000 -0700
--- token/ERC20/README.adoc 2022-08-11 21:28:00.000000000 -0700
+++ token/ERC20/README.adoc 2022-08-11 21:28:36.000000000 -0700
@@ -24,7 +24,7 @@
* {ERC20Votes}: support for voting and vote delegation.
* {ERC20VotesComp}: support for voting and vote delegation (compatible with Compound's token, with uint96 restrictions).
@ -719,8 +719,8 @@ diff -ruN token/ERC20/README.adoc token/ERC20/README.adoc
== Draft EIPs
diff -ruN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20FlashMint.sol
--- token/ERC20/extensions/ERC20FlashMint.sol 2022-08-11 21:13:55.000000000 -0700
+++ token/ERC20/extensions/ERC20FlashMint.sol 2022-08-11 21:15:52.000000000 -0700
--- token/ERC20/extensions/ERC20FlashMint.sol 2022-08-11 21:28:00.000000000 -0700
+++ token/ERC20/extensions/ERC20FlashMint.sol 2022-08-11 21:28:36.000000000 -0700
@@ -40,9 +40,11 @@
require(token == address(this), "ERC20FlashMint: wrong token");
// silence warning about unused variable without the addition of bytecode.
@ -736,7 +736,7 @@ diff -ruN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20
* implementation returns the address(0) which means the fee amount will be burnt.
diff -ruN token/ERC20/extensions/ERC20TokenizedVault.sol token/ERC20/extensions/ERC20TokenizedVault.sol
--- token/ERC20/extensions/ERC20TokenizedVault.sol 1969-12-31 16:00:00.000000000 -0800
+++ token/ERC20/extensions/ERC20TokenizedVault.sol 2022-08-11 21:15:52.000000000 -0700
+++ token/ERC20/extensions/ERC20TokenizedVault.sol 2022-08-11 21:28:36.000000000 -0700
@@ -0,0 +1,217 @@
+// SPDX-License-Identifier: MIT
+
@ -957,7 +957,7 @@ diff -ruN token/ERC20/extensions/ERC20TokenizedVault.sol token/ERC20/extensions/
+}
diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Votes.sol
--- token/ERC20/extensions/ERC20Votes.sol 2022-08-11 21:16:57.000000000 -0700
+++ token/ERC20/extensions/ERC20Votes.sol 2022-08-11 21:25:13.000000000 -0700
+++ token/ERC20/extensions/ERC20Votes.sol 2022-08-11 22:47:30.000000000 -0700
@@ -33,8 +33,8 @@
bytes32 private constant _DELEGATION_TYPEHASH =
keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)");
@ -1088,9 +1088,34 @@ diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Vote
return a + b;
}
diff -ruN token/ERC20/extensions/ERC20Wrapper.sol token/ERC20/extensions/ERC20Wrapper.sol
--- token/ERC20/extensions/ERC20Wrapper.sol 2022-08-11 21:13:55.000000000 -0700
+++ token/ERC20/extensions/ERC20Wrapper.sol 2022-08-11 21:15:52.000000000 -0700
@@ -55,7 +55,7 @@
--- token/ERC20/extensions/ERC20Wrapper.sol 2022-08-11 21:28:00.000000000 -0700
+++ token/ERC20/extensions/ERC20Wrapper.sol 2022-08-11 21:29:19.000000000 -0700
@@ -1,5 +1,5 @@
// SPDX-License-Identifier: MIT
-// OpenZeppelin Contracts (last updated v4.6.0) (token/ERC20/extensions/ERC20Wrapper.sol)
+// OpenZeppelin Contracts v4.4.1 (token/ERC20/extensions/ERC20Wrapper.sol)
pragma solidity ^0.8.0;
@@ -23,17 +23,6 @@
}
/**
- * @dev See {ERC20-decimals}.
- */
- function decimals() public view virtual override returns (uint8) {
- try IERC20Metadata(address(underlying)).decimals() returns (uint8 value) {
- return value;
- } catch {
- return super.decimals();
- }
- }
-
- /**
* @dev Allow a user to deposit underlying tokens and mint the corresponding number of wrapped tokens.
*/
function depositFor(address account, uint256 amount) public virtual returns (bool) {
@@ -55,7 +44,7 @@
* @dev Mint wrapped token to cover any underlyingTokens that would have been transferred by mistake. Internal
* function that can be exposed with access control if desired.
*/
@ -1100,7 +1125,7 @@ diff -ruN token/ERC20/extensions/ERC20Wrapper.sol token/ERC20/extensions/ERC20Wr
_mint(account, value);
return value;
diff -ruN token/ERC20/extensions/ERC4626.sol token/ERC20/extensions/ERC4626.sol
--- token/ERC20/extensions/ERC4626.sol 2022-08-11 21:13:55.000000000 -0700
--- token/ERC20/extensions/ERC4626.sol 2022-08-11 21:28:00.000000000 -0700
+++ token/ERC20/extensions/ERC4626.sol 1969-12-31 16:00:00.000000000 -0800
@@ -1,217 +0,0 @@
-// SPDX-License-Identifier: MIT
@ -1321,8 +1346,8 @@ diff -ruN token/ERC20/extensions/ERC4626.sol token/ERC20/extensions/ERC4626.sol
- }
-}
diff -ruN token/ERC20/utils/SafeERC20.sol token/ERC20/utils/SafeERC20.sol
--- token/ERC20/utils/SafeERC20.sol 2022-08-11 21:13:55.000000000 -0700
+++ token/ERC20/utils/SafeERC20.sol 2022-08-11 21:15:52.000000000 -0700
--- token/ERC20/utils/SafeERC20.sol 2022-08-11 21:28:00.000000000 -0700
+++ token/ERC20/utils/SafeERC20.sol 2022-08-11 21:28:36.000000000 -0700
@@ -4,7 +4,6 @@
pragma solidity ^0.8.0;
@ -1355,8 +1380,8 @@ diff -ruN token/ERC20/utils/SafeERC20.sol token/ERC20/utils/SafeERC20.sol
* @dev Imitates a Solidity high-level call (i.e. a regular function call to a contract), relaxing the requirement
* on the return value: the return value is optional (but if data is returned, it must not be false).
diff -ruN token/ERC721/extensions/draft-ERC721Votes.sol token/ERC721/extensions/draft-ERC721Votes.sol
--- token/ERC721/extensions/draft-ERC721Votes.sol 2022-08-11 21:13:55.000000000 -0700
+++ token/ERC721/extensions/draft-ERC721Votes.sol 2022-08-11 21:15:52.000000000 -0700
--- token/ERC721/extensions/draft-ERC721Votes.sol 2022-08-11 21:28:00.000000000 -0700
+++ token/ERC721/extensions/draft-ERC721Votes.sol 2022-08-11 21:28:36.000000000 -0700
@@ -34,7 +34,7 @@
/**
* @dev Returns the balance of `account`.
@ -1367,8 +1392,8 @@ diff -ruN token/ERC721/extensions/draft-ERC721Votes.sol token/ERC721/extensions/
}
}
diff -ruN utils/Address.sol utils/Address.sol
--- utils/Address.sol 2022-08-11 21:13:55.000000000 -0700
+++ utils/Address.sol 2022-08-11 21:15:52.000000000 -0700
--- utils/Address.sol 2022-08-11 21:28:00.000000000 -0700
+++ utils/Address.sol 2022-08-11 21:28:36.000000000 -0700
@@ -131,6 +131,7 @@
uint256 value,
string memory errorMessage
@ -1378,8 +1403,8 @@ diff -ruN utils/Address.sol utils/Address.sol
require(isContract(target), "Address: call to non-contract");
diff -ruN utils/math/Math.sol utils/math/Math.sol
--- utils/math/Math.sol 2022-08-11 21:13:55.000000000 -0700
+++ utils/math/Math.sol 2022-08-11 21:15:52.000000000 -0700
--- utils/math/Math.sol 2022-08-11 21:28:00.000000000 -0700
+++ utils/math/Math.sol 2022-08-11 21:28:36.000000000 -0700
@@ -149,78 +149,4 @@
}
return result;

5
certora/scripts/Round2/verifyERC20Votes.sh
Unescape View File

@ -2,12 +2,11 @@ certoraRun \
certora/harnesses/ERC20VotesHarness.sol \
--verify ERC20VotesHarness:certora/specs/ERC20Votes.spec \
--solc solc8.2 \
--disableLocalTypeChecking \
--optimistic_loop \
--settings -copyLoopUnroll=4 \
--cloud \
--send_only \
--msg "ERC20Votes" \
--msg "ERC20Votes $1" \
# --disableLocalTypeChecking \
# --staging "alex/new-dt-hashing-alpha" \

21
certora/specs/ERC20Votes.spec
Unescape View File

@ -29,9 +29,8 @@ ghost userVotes(address) returns uint224 {
}
// sums the total votes for all users
ghost totalVotes() returns mathint {
ghost totalVotes() returns uint224 {
init_state axiom totalVotes() == 0;
axiom totalVotes() >= 0;
}
ghost lastIndex(address) returns uint32;
// helper
@ -41,7 +40,7 @@ hook Sstore _checkpoints[KEY address account][INDEX uint32 index].votes uint224
userVotes@new(account) == newVotes;
havoc totalVotes assuming
totalVotes@new() == totalVotes@old() + to_mathint(newVotes) - to_mathint(userVotes(account));
totalVotes@new() == totalVotes@old() + newVotes - userVotes(account);
havoc lastIndex assuming
lastIndex@new(account) == index;
@ -68,9 +67,15 @@ hook Sstore _checkpoints[KEY address account][INDEX uint32 index].fromBlock uint
// sum of user balances is >= total amount of delegated votes
// fails on burn. This is because burn does not remove votes from the users
invariant votes_solvency()
to_mathint(totalSupply()) >= totalVotes()
totalSupply() >= to_uint256(totalVotes())
filtered { f -> f.selector != _burn(address, uint256).selector}
{ preserved with(env e) {
require forall address account. numCheckpoints(account) < 1000000;
} preserved burn(address a, uint256 amount) with(env e){
require _delegates(0) == 0;
require forall address a2. (_delegates(a) != _delegates(a2)) && (balanceOf(e, _delegates(a)) + balanceOf(e, _delegates(a2)) <= totalVotes());
require balanceOf(e, _delegates(a)) < totalVotes();
require amount < 100000;
}}
@ -146,10 +151,10 @@ rule transfer_safe() {
require numCheckpoints(delegates(b)) < 1000000;
uint256 votesA_pre = getVotes(delegates(a));
uint256 votesB_pre = getVotes(delegates(b));
mathint totalVotes_pre = totalVotes();
uint224 totalVotes_pre = totalVotes();
transferFrom(e, a, b, amount);
mathint totalVotes_post = totalVotes();
uint224 totalVotes_post = totalVotes();
uint256 votesA_post = getVotes(delegates(a));
uint256 votesB_post = getVotes(delegates(b));
// if an account that has not delegated transfers balance to an account that has, it will increase the total supply of votes
@ -308,7 +313,7 @@ rule mint_doesnt_increase_totalVotes() {
env e;
uint256 amount; address account;
mathint totalVotes_ = totalVotes();
uint224 totalVotes_ = totalVotes();
mint(e, account, amount);
@ -319,7 +324,7 @@ rule burn_doesnt_decrease_totalVotes() {
env e;
uint256 amount; address account;
mathint totalVotes_ = totalVotes();
uint224 totalVotes_ = totalVotes();
burn(e, account, amount);

Write Preview
Loading…
Cancel
Save