2023-12-14 07:53:57 +00:00
|
|
|
methods {
|
|
|
|
function balanceOf(address) external returns (uint) envfree;
|
|
|
|
function ownerOf(uint256 tokenId) external returns (address) envfree;
|
|
|
|
function transferable() external returns (bool) envfree;
|
|
|
|
function totalSupply() external returns (uint) envfree;
|
|
|
|
function maxSupply() external returns (uint) envfree;
|
2024-02-18 14:24:57 +00:00
|
|
|
function setMaxSupply(uint256 newMaxSupply) external returns (uint);
|
2024-02-11 13:22:32 +00:00
|
|
|
function mintTo(address[]) external;
|
2024-02-11 10:36:19 +00:00
|
|
|
function mintedCount() external returns (uint) envfree;
|
2024-02-11 13:22:32 +00:00
|
|
|
function countAddressOccurrences(address[], address) external returns (uint) envfree;
|
|
|
|
function _.onERC721Received(address, address, uint256, bytes) external => NONDET;
|
2024-02-11 10:36:19 +00:00
|
|
|
}
|
|
|
|
|
2024-02-11 13:22:32 +00:00
|
|
|
ghost mathint sumOfBalances {
|
|
|
|
init_state axiom sumOfBalances == 0;
|
|
|
|
}
|
2024-02-11 10:36:19 +00:00
|
|
|
|
2024-02-11 13:22:32 +00:00
|
|
|
hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE {
|
|
|
|
sumOfBalances = sumOfBalances - oldValue + newValue;
|
|
|
|
}
|
2024-02-11 10:36:19 +00:00
|
|
|
|
2024-02-11 13:22:32 +00:00
|
|
|
hook Sload uint256 balance _balances[KEY address addr] STORAGE {
|
|
|
|
require sumOfBalances >= to_mathint(balance);
|
|
|
|
}
|
2024-02-11 10:36:19 +00:00
|
|
|
|
2024-02-18 14:24:57 +00:00
|
|
|
function safeAssumptions() {
|
|
|
|
requireInvariant mintCountGreaterEqualTotalSupplyAndTotalSupplyEqBalances();
|
|
|
|
}
|
|
|
|
|
2024-02-11 13:22:32 +00:00
|
|
|
invariant mintCountGreaterEqualTotalSupplyAndTotalSupplyEqBalances()
|
|
|
|
to_mathint(mintedCount()) >= to_mathint(totalSupply()) &&
|
|
|
|
to_mathint(totalSupply()) == sumOfBalances;
|
2024-02-11 10:36:19 +00:00
|
|
|
|
2024-02-11 13:22:32 +00:00
|
|
|
rule integrityOfMintTo {
|
|
|
|
requireInvariant mintCountGreaterEqualTotalSupplyAndTotalSupplyEqBalances();
|
2024-02-11 10:36:19 +00:00
|
|
|
|
2024-02-11 13:22:32 +00:00
|
|
|
address[] addresses;
|
|
|
|
env e;
|
2024-02-11 10:36:19 +00:00
|
|
|
|
2024-02-11 13:22:32 +00:00
|
|
|
mathint totalSupply_before = totalSupply();
|
|
|
|
mathint maxSupply = to_mathint(maxSupply());
|
|
|
|
|
|
|
|
address addr;
|
2024-02-11 10:36:19 +00:00
|
|
|
|
2024-02-11 13:22:32 +00:00
|
|
|
require totalSupply_before < maxSupply;
|
|
|
|
require totalSupply_before + addresses.length <= maxSupply;
|
|
|
|
|
|
|
|
mathint balance_addr_before = balanceOf(addr);
|
|
|
|
mathint count = countAddressOccurrences(addresses, addr);
|
|
|
|
mintTo(e, addresses);
|
2024-02-11 10:36:19 +00:00
|
|
|
|
2024-02-11 13:22:32 +00:00
|
|
|
mathint totalSupply_after = totalSupply();
|
|
|
|
mathint balance_addr_after = balanceOf(addr);
|
2024-02-11 10:36:19 +00:00
|
|
|
|
2024-02-11 13:22:32 +00:00
|
|
|
assert totalSupply_after == totalSupply_before + addresses.length;
|
|
|
|
assert balance_addr_after == balance_addr_before + count;
|
2024-02-11 10:36:19 +00:00
|
|
|
}
|
|
|
|
|
2024-02-18 14:24:57 +00:00
|
|
|
rule maxSupplyCannotBeLowerThanMintedCount() {
|
|
|
|
require maxSupply() >= mintedCount();
|
2024-02-11 10:36:19 +00:00
|
|
|
|
2024-02-18 14:24:57 +00:00
|
|
|
env e;
|
|
|
|
uint256 newMaxSupply;
|
|
|
|
|
|
|
|
setMaxSupply(e, newMaxSupply);
|
2024-02-11 10:36:19 +00:00
|
|
|
|
2024-02-18 14:24:57 +00:00
|
|
|
assert maxSupply() >= mintedCount();
|
|
|
|
}
|
|
|
|
|
|
|
|
rule maxSupplyNotLowerThanTotalSupply(env e, method f) {
|
|
|
|
require maxSupply() >= totalSupply();
|
|
|
|
|
|
|
|
calldataarg args;
|
|
|
|
f(e, args); // call all public/external functions of a contract
|
|
|
|
|
|
|
|
assert maxSupply() >= totalSupply();
|
|
|
|
}
|
2024-02-11 10:36:19 +00:00
|
|
|
|
|
|
|
rule mintToReverts() {
|
|
|
|
address[] addresses;
|
|
|
|
env e;
|
|
|
|
|
|
|
|
mathint supply_before = totalSupply();
|
|
|
|
mathint max_supply = maxSupply();
|
|
|
|
mathint minted_count = mintedCount();
|
|
|
|
|
|
|
|
require supply_before <= max_supply;
|
|
|
|
require minted_count >= supply_before;
|
|
|
|
|
|
|
|
mintTo@withrevert(e, addresses);
|
|
|
|
|
|
|
|
bool reverted = lastReverted;
|
|
|
|
|
|
|
|
assert (supply_before + addresses.length > max_supply) => reverted;
|
|
|
|
|
|
|
|
satisfy supply_before == max_supply && addresses.length > 0 && reverted;
|
|
|
|
}
|
|
|
|
|
|
|
|
rule mintToRelations() {
|
|
|
|
address[] addresses_1;
|
|
|
|
address[] addresses_2;
|
|
|
|
env e;
|
|
|
|
|
|
|
|
require addresses_1.length == 2;
|
|
|
|
require addresses_1.length == addresses_2.length;
|
|
|
|
|
|
|
|
require addresses_1[0] != addresses_1[1];
|
|
|
|
require addresses_1[0] == addresses_2[1];
|
|
|
|
require addresses_1[1] == addresses_2[0];
|
|
|
|
|
|
|
|
mathint supply_before = totalSupply();
|
|
|
|
mathint max_supply = maxSupply();
|
|
|
|
mathint minted_count = mintedCount();
|
|
|
|
|
|
|
|
require supply_before <= max_supply;
|
|
|
|
require minted_count >= supply_before;
|
|
|
|
|
|
|
|
address a;
|
|
|
|
|
|
|
|
storage s1 = lastStorage;
|
|
|
|
mintTo(e, addresses_1);
|
|
|
|
mathint balance_s1 = balanceOf(a);
|
|
|
|
|
|
|
|
mintTo(e, addresses_2) at s1;
|
|
|
|
|
|
|
|
mathint balance_s2 = balanceOf(a);
|
|
|
|
assert balance_s1 == balance_s2;
|
2023-12-14 07:53:57 +00:00
|
|
|
}
|
|
|
|
|
|
|
|
rule shouldPass {
|
|
|
|
assert true;
|
|
|
|
}
|
|
|
|
|
|
|
|
/* rule sanity(env e, method f) { */
|
|
|
|
/* calldataarg args; */
|
|
|
|
/* f(e, args); */
|
|
|
|
/* assert false; */
|
|
|
|
/* } */
|