update certora config and add a rule for setMaxSupply
This commit is contained in:
parent
36efa32a9c
commit
77b799111d
|
@ -1,8 +1,15 @@
|
|||
{
|
||||
"files": ["contracts/tokens/CollectibleV1.sol", "certora/harness/CollectibleV1Harness.sol"],
|
||||
"files": [
|
||||
"contracts/tokens/CollectibleV1.sol",
|
||||
"certora/harness/CollectibleV1Harness.sol",
|
||||
"contracts/tokens/OwnerToken.sol",
|
||||
"contracts/tokens/MasterToken.sol"
|
||||
],
|
||||
"msg": "Verifying CollectibleV1.sol",
|
||||
"rule_sanity": "basic",
|
||||
"verify": "CollectibleV1Harness:certora/specs/CollectibleV1.spec",
|
||||
"wait_for_results": "all",
|
||||
"packages": ["@openzeppelin=lib/openzeppelin-contracts"]
|
||||
"link": ["CollectibleV1Harness:ownerToken=OwnerToken", "CollectibleV1Harness:masterToken=MasterToken"],
|
||||
"packages": ["@openzeppelin=lib/openzeppelin-contracts"],
|
||||
"optimistic_loop": true,
|
||||
"loop_iter": "3"
|
||||
}
|
||||
|
|
|
@ -4,6 +4,7 @@ methods {
|
|||
function transferable() external returns (bool) envfree;
|
||||
function totalSupply() external returns (uint) envfree;
|
||||
function maxSupply() external returns (uint) envfree;
|
||||
function setMaxSupply(uint256 newMaxSupply) external returns (uint);
|
||||
function mintTo(address[]) external;
|
||||
function mintedCount() external returns (uint) envfree;
|
||||
function countAddressOccurrences(address[], address) external returns (uint) envfree;
|
||||
|
@ -22,6 +23,10 @@ hook Sload uint256 balance _balances[KEY address addr] STORAGE {
|
|||
require sumOfBalances >= to_mathint(balance);
|
||||
}
|
||||
|
||||
function safeAssumptions() {
|
||||
requireInvariant mintCountGreaterEqualTotalSupplyAndTotalSupplyEqBalances();
|
||||
}
|
||||
|
||||
invariant mintCountGreaterEqualTotalSupplyAndTotalSupplyEqBalances()
|
||||
to_mathint(mintedCount()) >= to_mathint(totalSupply()) &&
|
||||
to_mathint(totalSupply()) == sumOfBalances;
|
||||
|
@ -51,10 +56,25 @@ rule integrityOfMintTo {
|
|||
assert balance_addr_after == balance_addr_before + count;
|
||||
}
|
||||
|
||||
rule maxSupplyCannotBeLowerThanMintedCount() {
|
||||
require maxSupply() >= mintedCount();
|
||||
|
||||
//rule integrityOfMintToWithEmptyArray{
|
||||
//}
|
||||
env e;
|
||||
uint256 newMaxSupply;
|
||||
|
||||
setMaxSupply(e, newMaxSupply);
|
||||
|
||||
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();
|
||||
}
|
||||
|
||||
rule mintToReverts() {
|
||||
address[] addresses;
|
||||
|
@ -116,90 +136,3 @@ rule shouldPass {
|
|||
/* f(e, args); */
|
||||
/* assert false; */
|
||||
/* } */
|
||||
|
||||
/// rule mintTo_FromOwner {
|
||||
/// // address owner;
|
||||
/// address recipient_1;
|
||||
/// address recipient_2;
|
||||
///
|
||||
/// env e;
|
||||
/// require recipient_1 != recipient_2;
|
||||
/// // require e.msg.sender == owner;
|
||||
/// // require owner() == owner;
|
||||
/// require maxSupply() == 100000;
|
||||
/// require totalSupply() == 0;
|
||||
/// require balanceOf(recipient_1) == 0;
|
||||
/// require balanceOf(recipient_2) == 0;
|
||||
///
|
||||
/// assert balanceOf(recipient_1) == 0, "balance of recipient_1 should be 0";
|
||||
/// assert balanceOf(recipient_2) == 0, "balance of recipient_2 should be 0";
|
||||
///
|
||||
/// mintTo(e, [recipient_1, recipient_2]);
|
||||
///
|
||||
/// assert balanceOf(recipient_1) == 1, "balance of recipient_1 should be 1";
|
||||
/// assert balanceOf(recipient_2) == 1, "balance of recipient_2 should be 1";
|
||||
/// }
|
||||
///
|
||||
/// rule transferNFT_validOwner {
|
||||
/// address sender;
|
||||
/// address recipient;
|
||||
/// uint token_id;
|
||||
///
|
||||
/// env e;
|
||||
/// require e.msg.sender == sender;
|
||||
/// require sender != recipient;
|
||||
/// require ownerOf(token_id) == sender;
|
||||
/// require transferable() == true;
|
||||
///
|
||||
/// mathint balance_sender_before = balanceOf(sender);
|
||||
/// mathint balance_recipient_before = balanceOf(recipient);
|
||||
///
|
||||
/// transferFrom(e, sender, recipient, token_id);
|
||||
///
|
||||
/// assert ownerOf(token_id) == recipient;
|
||||
/// assert balanceOf(sender) == assert_uint256(balance_sender_before - 1);
|
||||
/// /* assert balanceOf(recipient) == balance_recipient_before + 1; */
|
||||
/// }
|
||||
///
|
||||
/// rule transferNFT_invalidOwner {
|
||||
/// address sender;
|
||||
/// address recipient;
|
||||
/// uint token_id;
|
||||
///
|
||||
/// env e;
|
||||
/// require e.msg.sender == sender;
|
||||
/// require sender != recipient;
|
||||
/// require ownerOf(token_id) != sender;
|
||||
/// require transferable() == true;
|
||||
///
|
||||
/// transferFrom@withrevert(e, sender, recipient, token_id);
|
||||
/// assert lastReverted, "transfer should revert when the sender is not the owner of tokenId";
|
||||
/// }
|
||||
///
|
||||
/// rule transferSoulbound {
|
||||
/// address sender;
|
||||
/// address recipient;
|
||||
/// uint token_id;
|
||||
///
|
||||
/// env e;
|
||||
/// require e.msg.sender == sender;
|
||||
/// require sender != recipient;
|
||||
/// require ownerOf(token_id) == sender;
|
||||
/// require transferable() == false;
|
||||
///
|
||||
/// mathint balance_sender_before = balanceOf(sender);
|
||||
/// mathint balance_recipient_before = balanceOf(recipient);
|
||||
///
|
||||
/// transferFrom@withrevert(e, sender, recipient, token_id);
|
||||
///
|
||||
/// assert lastReverted, "transfer should revert if it's a Soulbound token";
|
||||
/// }
|
||||
///
|
||||
/// 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();
|
||||
/// }
|
||||
|
|
Loading…
Reference in New Issue