NoBey/openzeppelin-contracts
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Merge branch 'certora/erc1155ext' of github.com:Certora/openzeppelin-contracts into certora/erc1155ext

Browse Source
This commit is contained in:
Thomas Adams
2022-05-26 11:21:55 -07:00
parent 428197be69 5e69b54af1
commit da1cda69bf
433 changed files with 12104 additions and 26644 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
certora/specs/GovernorBase.spec
View File

@ -177,11 +177,11 @@ rule executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId, env e, method f){
/*
* A user cannot vote twice
*/
// Checked for castVote only. all 3 castVote functions call _castVote, so the completness of the verification is counted on
// the fact that the 3 functions themselves makes no chages, but rather call an internal function to execute.
// Checked for castVote only. all 3 castVote functions call _castVote, so the completeness of the verification is counted on
// the fact that the 3 functions themselves makes no changes, but rather call an internal function to execute.
// That means that we do not check those 3 functions directly, however for castVote & castVoteWithReason it is quite trivial
// to understand why this is ok. For castVoteBySig we basically assume that the signature referendum is correct without checking it.
// We could check each function seperately and pass the rule, but that would have uglyfied the code with no concrete
// We could check each function separately and pass the rule, but that would have uglyfied the code with no concrete
// benefit, as it is evident that nothing is happening in the first 2 functions (calling a view function), and we do not desire to check the signature verification.
rule doubleVoting(uint256 pId, uint8 sup, method f) {
env e;

10
certora/specs/GovernorCountingSimple.spec
View File

@ -123,11 +123,11 @@ invariant OneIsNotMoreThanAll(uint256 pId)
/*
* Only sender's voting status can be changed by execution of any cast vote function
*/
// Checked for castVote only. all 3 castVote functions call _castVote, so the completness of the verification is counted on
// the fact that the 3 functions themselves makes no chages, but rather call an internal function to execute.
// Checked for castVote only. all 3 castVote functions call _castVote, so the completeness of the verification is counted on
// the fact that the 3 functions themselves makes no changes, but rather call an internal function to execute.
// That means that we do not check those 3 functions directly, however for castVote & castVoteWithReason it is quite trivial
// to understand why this is ok. For castVoteBySig we basically assume that the signature referendum is correct without checking it.
// We could check each function seperately and pass the rule, but that would have uglyfied the code with no concrete
// We could check each function separately and pass the rule, but that would have uglyfied the code with no concrete
// benefit, as it is evident that nothing is happening in the first 2 functions (calling a view function), and we do not desire to check the signature verification.
rule noVoteForSomeoneElse(uint256 pId, uint8 sup, method f) {
env e; calldataarg args;
@ -201,7 +201,7 @@ rule privilegedOnlyNumerator(method f, uint256 newQuorumNumerator){
uint256 quorumNumAfter = quorumNumerator(e);
address executorCheck = getExecutor(e);
assert quorumNumBefore != quorumNumAfter => e.msg.sender == executorCheck, "non priveleged user changed quorum numerator";
assert quorumNumBefore != quorumNumAfter => e.msg.sender == executorCheck, "non privileged user changed quorum numerator";
}
rule privilegedOnlyTimelock(method f, uint256 newQuorumNumerator){
@ -213,5 +213,5 @@ rule privilegedOnlyTimelock(method f, uint256 newQuorumNumerator){
uint256 timelockAfter = timelock(e);
assert timelockBefore != timelockAfter => e.msg.sender == timelockBefore, "non priveleged user changed timelock";
assert timelockBefore != timelockAfter => e.msg.sender == timelockBefore, "non privileged user changed timelock";
}