fix integrityOfMintTo
This commit is contained in:
parent
67aa09e101
commit
36efa32a9c
|
@ -1,8 +1,8 @@
|
|||
{
|
||||
"files": ["contracts/tokens/CollectibleV1.sol"],
|
||||
"files": ["contracts/tokens/CollectibleV1.sol", "certora/harness/CollectibleV1Harness.sol"],
|
||||
"msg": "Verifying CollectibleV1.sol",
|
||||
"rule_sanity": "basic",
|
||||
"verify": "CollectibleV1:certora/specs/CollectibleV1.spec",
|
||||
"verify": "CollectibleV1Harness:certora/specs/CollectibleV1.spec",
|
||||
"wait_for_results": "all",
|
||||
"packages": ["@openzeppelin=lib/openzeppelin-contracts"]
|
||||
}
|
||||
|
|
|
@ -0,0 +1,44 @@
|
|||
// SPDX-License-Identifier: Mozilla Public License 2.0
|
||||
pragma solidity ^0.8.17;
|
||||
|
||||
import {CollectibleV1} from "../../contracts/tokens/CollectibleV1.sol";
|
||||
|
||||
contract CollectibleV1Harness is CollectibleV1 {
|
||||
constructor(
|
||||
string memory name,
|
||||
string memory symbol,
|
||||
uint256 maxSupply,
|
||||
bool remoteBurnable,
|
||||
bool transferable,
|
||||
string memory baseURI,
|
||||
address ownerToken,
|
||||
address masterToken
|
||||
)
|
||||
CollectibleV1(
|
||||
name,
|
||||
symbol,
|
||||
maxSupply,
|
||||
remoteBurnable,
|
||||
transferable,
|
||||
baseURI,
|
||||
ownerToken,
|
||||
masterToken
|
||||
)
|
||||
{}
|
||||
|
||||
/**
|
||||
* @notice A helper function to count the number of occurrences of an address in a list.
|
||||
*/
|
||||
function countAddressOccurrences(
|
||||
address[] memory list,
|
||||
address addr
|
||||
) external pure returns (uint) {
|
||||
uint256 count = 0;
|
||||
for (uint256 i = 0; i < list.length; i++) {
|
||||
if (list[i] == addr) {
|
||||
count++;
|
||||
}
|
||||
}
|
||||
return count;
|
||||
}
|
||||
}
|
|
@ -1,6 +1,7 @@
|
|||
certoraRun \
|
||||
contracts/tokens/CollectibleV1.sol \
|
||||
--verify CollectibleV1:certora/specs/CollectibleV1.spec \
|
||||
certora/harness/CollectibleV1Harness.sol \
|
||||
--verify CollectibleV1Harness:certora/specs/CollectibleV1.spec \
|
||||
--packages @openzeppelin=lib/openzeppelin-contracts \
|
||||
--optimistic_loop \
|
||||
--loop_iter 3 \
|
||||
|
|
|
@ -4,36 +4,51 @@ methods {
|
|||
function transferable() external returns (bool) envfree;
|
||||
function totalSupply() external returns (uint) envfree;
|
||||
function maxSupply() external returns (uint) envfree;
|
||||
function mintTo(address[]) external;
|
||||
function mintedCount() external returns (uint) envfree;
|
||||
function countAddressOccurrences(address[], address) external returns (uint) envfree;
|
||||
function _.onERC721Received(address, address, uint256, bytes) external => NONDET;
|
||||
}
|
||||
|
||||
rule integrityOfMintTo() {
|
||||
ghost mathint sumOfBalances {
|
||||
init_state axiom sumOfBalances == 0;
|
||||
}
|
||||
|
||||
hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE {
|
||||
sumOfBalances = sumOfBalances - oldValue + newValue;
|
||||
}
|
||||
|
||||
hook Sload uint256 balance _balances[KEY address addr] STORAGE {
|
||||
require sumOfBalances >= to_mathint(balance);
|
||||
}
|
||||
|
||||
invariant mintCountGreaterEqualTotalSupplyAndTotalSupplyEqBalances()
|
||||
to_mathint(mintedCount()) >= to_mathint(totalSupply()) &&
|
||||
to_mathint(totalSupply()) == sumOfBalances;
|
||||
|
||||
rule integrityOfMintTo {
|
||||
requireInvariant mintCountGreaterEqualTotalSupplyAndTotalSupplyEqBalances();
|
||||
|
||||
address[] addresses;
|
||||
uint index;
|
||||
env e;
|
||||
|
||||
require addresses.length > 0;
|
||||
require index >= 0 && index < addresses.length;
|
||||
mathint totalSupply_before = totalSupply();
|
||||
mathint maxSupply = to_mathint(maxSupply());
|
||||
|
||||
address addr;
|
||||
|
||||
mathint supply_before = totalSupply();
|
||||
mathint max_supply = maxSupply();
|
||||
mathint minted_count = mintedCount();
|
||||
|
||||
address a = addresses[index];
|
||||
mathint balance_before = balanceOf(a);
|
||||
|
||||
require supply_before <= max_supply;
|
||||
require minted_count >= supply_before;
|
||||
require totalSupply_before < maxSupply;
|
||||
require totalSupply_before + addresses.length <= maxSupply;
|
||||
|
||||
mathint balance_addr_before = balanceOf(addr);
|
||||
mathint count = countAddressOccurrences(addresses, addr);
|
||||
mintTo(e, addresses);
|
||||
|
||||
mathint supply_after = totalSupply();
|
||||
mathint totalSupply_after = totalSupply();
|
||||
mathint balance_addr_after = balanceOf(addr);
|
||||
|
||||
assert supply_after <= max_supply;
|
||||
assert supply_after == supply_before + to_mathint(addresses.length);
|
||||
|
||||
assert to_mathint(balanceOf(a)) > balance_before;
|
||||
assert totalSupply_after == totalSupply_before + addresses.length;
|
||||
assert balance_addr_after == balance_addr_before + count;
|
||||
}
|
||||
|
||||
|
||||
|
|
|
@ -82,7 +82,7 @@ abstract contract BaseToken is Context, ERC721Enumerable, CommunityOwnable {
|
|||
*
|
||||
*/
|
||||
function mintTo(address[] memory addresses) public onlyCommunityOwnerOrTokenMaster {
|
||||
if (_tokenIdTracker.current() + addresses.length > maxSupply) {
|
||||
if (mintedCount() + addresses.length > maxSupply) {
|
||||
revert BaseToken_MaxSupplyReached();
|
||||
}
|
||||
_mintTo(addresses);
|
||||
|
|
Loading…
Reference in New Issue