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

CI preparations

Browse Source
This commit is contained in:
Aleksander Kryukov
2022-04-08 20:52:38 +01:00
parent 163a76f436
commit 66c72f2b5d
9 changed files with 40 additions and 41 deletions
Download Patch File Download Diff File Expand all files Collapse all files

5
certora/scripts/verifyAccessControl.sh
View File

@ -3,7 +3,6 @@ certoraRun \
--verify AccessControlHarness:certora/specs/AccessControl.spec \
--solc solc8.2 \
--optimistic_loop \
--staging \
--rule_sanity \
--msg "modifier check"
--cloud \
--msg "AccessControl verification"

5
certora/scripts/verifyAllSasha.sh Normal file
View File

@ -0,0 +1,5 @@
sh certora/scripts/verifyTimelock.sh
sh certora/scripts/verifyERC1155.sh
sh certora/scripts/verifyERC20FlashMint.sh
sh certora/scripts/verifyERC20Wrapper.sh
sh certora/scripts/verifyAccessControl.sh

6
certora/scripts/verifyERC1155.sh
View File

@ -4,8 +4,6 @@ certoraRun \
--solc solc8.2 \
--optimistic_loop \
--loop_iter 3 \
--staging \
--rule_sanity \
--rule "$1" \
--msg "$1 check"
--cloud \
--msg "ERC1155 verification"

5
certora/scripts/verifyERC20FlashMint.sh
View File

@ -4,7 +4,6 @@ certoraRun \
--verify ERC20FlashMintHarness:certora/specs/ERC20FlashMint.spec \
--solc solc8.2 \
--optimistic_loop \
--staging \
--rule_sanity \
--msg "flashMint"
--cloud \
--msg "ERC20FlashMint verification"

5
certora/scripts/verifyERC20Wrapper.sh
View File

@ -4,7 +4,6 @@ certoraRun \
--verify ERC20WrapperHarness:certora/specs/ERC20Wrapper.spec \
--solc solc8.2 \
--optimistic_loop \
--staging \
--rule_sanity \
--msg "ERC20wrapper spec"
--cloud \
--msg "ERC20Wrapper verification"

4
certora/scripts/verifyTimelock.sh
View File

@ -5,8 +5,6 @@ certoraRun \
--optimistic_loop \
--loop_iter 3 \
--staging alex/new-dt-hashing-alpha \
--rule_sanity \
--settings -byteMapHashingPrecision=32 \
--rule "$1" \
--msg "$1"
--msg "TimelockController verification"

1
certora/specs/ERC20Wrapper.spec
View File

@ -195,6 +195,7 @@ rule recoverSpec(env e){
uint256 wrapperTotalBefore = totalSupply(e);
uint256 wrapperUserBalanceBefore = balanceOf(e, account);
uint256 wrapperSenderBalanceBefore = balanceOf(e, e.msg.sender);
uint256 underlyingThisBalanceBefore = underlyingBalanceOf(currentContract);
mathint value = underlyingThisBalanceBefore - wrapperTotalBefore;

26
certora/specs/RulesInProgress.spec
View File

@ -136,4 +136,28 @@ rule possibleTotalVotes(uint256 pId, uint8 sup, env e, method f) {
uint256 ps = proposalSnapshot(pId);
assert tracked_weight(pId) <= erc20votes.getPastTotalSupply(e, proposalSnapshot(pId)), "bla bla bla";
}
}
/////////////////// 2nd iteration with OZ //////////////////////////
// STATUS - in progress
// execute() is the only way to set timestamp to 1
rule getTimestampOnlyChange(method f, env e){
bytes32 id;
address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt; uint256 delay;
address[] targets; uint256[] values; bytes[] datas;
require (targets[0] == target && values[0] == value && datas[0] == data)
|| (targets[1] == target && values[1] == value && datas[1] == data)
|| (targets[2] == target && values[2] == value && datas[2] == data);
hashIdCorrelation(id, target, value, data, predecessor, salt);
executionsCall(f, e, target, value, data, predecessor, salt, delay, targets, values, datas);
assert getTimestamp(id) == 1 => f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector
|| f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector, "Did you find a way to break the system?";
}

24
certora/specs/TimelockController.spec
View File

@ -335,27 +335,3 @@ rule cancelChange(env e){
assert id != otherId => otherIdTimestampBefore == getTimestamp(otherId), "Master of puppets, I'm pulling your strings";
}
// STATUS - in progress
// execute() is the only way to set timestamp to 1
rule getTimestampOnlyChange(method f, env e){
bytes32 id;
address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt; uint256 delay;
address[] targets; uint256[] values; bytes[] datas;
require (targets[0] == target && values[0] == value && datas[0] == data)
|| (targets[1] == target && values[1] == value && datas[1] == data)
|| (targets[2] == target && values[2] == value && datas[2] == data);
hashIdCorrelation(id, target, value, data, predecessor, salt);
executionsCall(f, e, target, value, data, predecessor, salt, delay, targets, values, datas);
assert getTimestamp(id) == 1 => f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector
|| f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector, "Did you find a way to break the system?";
}