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

Update certora-cli to 7.3.0

Browse Source
This commit is contained in:
ernestognw
2024-04-18 10:53:54 -06:00
parent 11dc5e3809
commit 1e811d34d2
3 changed files with 6 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
certora/specs/ERC20.spec
View File

@ -23,11 +23,11 @@ ghost mathint sumOfBalances {
// overflows Alice's balance when receiving a transfer. This is not possible unless the contract is deployed into an
// already used address (or upgraded from corrupted state).
// We restrict such behavior by making sure no balance is greater than the sum of balances.
hook Sload uint256 balance _balances[KEY address addr] STORAGE {
hook Sload uint256 balance _balances[KEY address addr] {
require sumOfBalances >= to_mathint(balance);
}
hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE {
hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) {
sumOfBalances = sumOfBalances - oldValue + newValue;
}

6
certora/specs/ERC721.spec
View File

@ -113,7 +113,7 @@ ghost mapping(address => mathint) _ownedByUser {
init_state axiom forall address a. _ownedByUser[a] == 0;
}
hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) STORAGE {
hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) {
_ownedByUser[newOwner] = _ownedByUser[newOwner] + to_mathint(newOwner != 0 ? 1 : 0);
_ownedByUser[oldOwner] = _ownedByUser[oldOwner] - to_mathint(oldOwner != 0 ? 1 : 0);
_ownedTotal = _ownedTotal + to_mathint(newOwner != 0 ? 1 : 0) - to_mathint(oldOwner != 0 ? 1 : 0);
@ -132,13 +132,13 @@ ghost mapping(address => mathint) _balances {
init_state axiom forall address a. _balances[a] == 0;
}
hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE {
hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) {
_supply = _supply - oldValue + newValue;
}
// TODO: This used to not be necessary. We should try to remove it. In order to do so, we will probably need to add
// many "preserved" directive that require the "balanceOfConsistency" invariant on the accounts involved.
hook Sload uint256 value _balances[KEY address user] STORAGE {
hook Sload uint256 value _balances[KEY address user] {
require _balances[user] == to_mathint(value);
}

2
requirements.txt
View File

@ -1 +1 @@
certora-cli==4.13.1
certora-cli==7.3.0