105 lines
3.1 KiB
Plaintext
105 lines
3.1 KiB
Plaintext
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;
|
|
}
|
|
|
|
rule shouldPass {
|
|
assert true;
|
|
}
|
|
|
|
/* rule sanity(env e, method f) { */
|
|
/* calldataarg args; */
|
|
/* 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();
|
|
/// }
|