methods {
    isApprovedForAll(address, address) returns(bool) envfree
    balanceOf(address, uint256) returns(uint256) envfree
    balanceOfBatch(address[], uint256[]) returns(uint256[]) envfree
    _doSafeBatchTransferAcceptanceCheck(address, address, address, uint256[], uint256[], bytes) envfree
    _doSafeTransferAcceptanceCheck(address, address, address, uint256, uint256, bytes) envfree

    setApprovalForAll(address, bool)
    safeTransferFrom(address, address, uint256, uint256, bytes)
    safeBatchTransferFrom(address, address, uint256[], uint256[], bytes)
    mint(address, uint256, uint256, bytes)
    mintBatch(address, uint256[], uint256[], bytes)
    burn(address, uint256, uint256)
    burnBatch(address, uint256[], uint256[])
}


/////////////////////////////////////////////////
// Approval (4/4)
/////////////////////////////////////////////////


// STATUS - verified
// Function $f, which is not setApprovalForAll, should not change approval
rule unexpectedAllowanceChange(method f, env e) filtered { f -> f.selector != setApprovalForAll(address, bool).selector } {
    address account; address operator;
    bool approveBefore = isApprovedForAll(account, operator);

    calldataarg args;
    f(e, args);

    bool approveAfter = isApprovedForAll(account, operator);

    assert approveBefore == approveAfter, "You couldn't get king's approval this way!";
}


// STATUS - verified
// approval can be changed only by owner
rule onlyOwnerCanApprove(env e){
    address owner; address operator; bool approved;

    bool aprovalBefore = isApprovedForAll(owner, operator);

    setApprovalForAll(e, operator, approved);

    bool aprovalAfter = isApprovedForAll(owner, operator);

    assert aprovalBefore != aprovalAfter => owner == e.msg.sender, "There should be only one owner";
}


// STATUS - verified
// Check that isApprovedForAll() revertes in planned scenarios and no more.
rule approvalRevertCases(env e){
    address account; address operator;
    isApprovedForAll@withrevert(account, operator);
    assert !lastReverted, "Houston, we have a problem";
}


// STATUS - verified
// setApproval changes only one approval
rule onlyOneAllowanceChange(method f, env e) {
    address owner; address operator; address user;
    bool approved;

    bool userApproveBefore = isApprovedForAll(owner, user);

    setApprovalForAll(e, operator, approved);

    bool userApproveAfter = isApprovedForAll(owner, user);

    assert userApproveBefore != userApproveAfter => (e.msg.sender == owner && operator == user), "Imposter!";
}



/////////////////////////////////////////////////
// Balance (3/3)
/////////////////////////////////////////////////


// STATUS - verified
// Function $f, which is not one of transfers, mints and burns, should not change balanceOf of a user
rule unexpectedBalanceChange(method f, env e)
    filtered { f -> f.selector != safeTransferFrom(address, address, uint256, uint256, bytes).selector
                        && f.selector != safeBatchTransferFrom(address, address, uint256[], uint256[], bytes).selector
                        && f.selector != mint(address, uint256, uint256, bytes).selector
                        && f.selector != mintBatch(address, uint256[], uint256[], bytes).selector
                        && f.selector != burn(address, uint256, uint256).selector
                        && f.selector != burnBatch(address, uint256[], uint256[]).selector } {
    address from; uint256 id;
    uint256 balanceBefore = balanceOf(from, id);

    calldataarg args;
    f(e, args);

    uint256 balanceAfter = balanceOf(from, id);

    assert balanceBefore == balanceAfter, "How you dare to take my money?";
}


// STATUS - verified
// Check that `balanceOf()` revertes in planned scenarios and no more (only if `account` is 0)
rule balanceOfRevertCases(env e){
    address account; uint256 id;
    balanceOf@withrevert(account, id);
    assert lastReverted => account == 0, "Houston, we have a problem";
}


// STATUS - verified
// Check that `balanceOfBatch()` revertes in planned scenarios and no more (only if at least one of `account`s is 0)
rule balanceOfBatchRevertCases(env e){
    address[] accounts; uint256[] ids;
    address account1; address account2; address account3;
    uint256 id1; uint256 id2; uint256 id3;

    require accounts.length == 3;
    require ids.length == 3;

    require accounts[0] == account1; require accounts[1] == account2; require accounts[2] == account3;

    balanceOfBatch@withrevert(accounts, ids);
    assert lastReverted => (account1 == 0 || account2 == 0 || account3 == 0), "Houston, we have a problem";
}



/////////////////////////////////////////////////
// Transfer (13/13)
/////////////////////////////////////////////////


// STATUS - verified
// transfer additivity
rule transferAdditivity(env e){
    address from; address to; uint256 id; bytes data;
    uint256 amount; uint256 amount1; uint256 amount2;
    require amount == amount1 + amount2;

    storage initialStorage = lastStorage;

    safeTransferFrom(e, from, to, id, amount, data);

    uint256 balanceAfterSingleTransaction = balanceOf(to, id);

    safeTransferFrom(e, from, to, id, amount1, data) at initialStorage;
    safeTransferFrom(e, from, to, id, amount2, data);

    uint256 balanceAfterDoubleTransaction = balanceOf(to, id);

    assert balanceAfterSingleTransaction == balanceAfterDoubleTransaction, "Not additive";
}


// STATUS - verified
// safeTransferFrom updates `from` and `to` balances
rule transferCorrectness(env e){
    address from; address to; uint256 id; uint256 amount; bytes data;

    require to != from;

    uint256 fromBalanceBefore = balanceOf(from, id);
    uint256 toBalanceBefore = balanceOf(to, id);

    safeTransferFrom(e, from, to, id, amount, data);

    uint256 fromBalanceAfter = balanceOf(from, id);
    uint256 toBalanceAfter = balanceOf(to, id);

    assert fromBalanceBefore == fromBalanceAfter + amount, "Something wet wrong";
    assert toBalanceBefore == toBalanceAfter - amount, "Something wet wrong";
}


// STATUS - verified
// safeBatchTransferFrom updates `from` and `to` balances)
rule transferBatchCorrectness(env e){
    address from; address to; uint256[] ids; uint256[] amounts; bytes data;
    uint256 idToCheck1; uint256 amountToCheck1;
    uint256 idToCheck2; uint256 amountToCheck2;
    uint256 idToCheck3; uint256 amountToCheck3;

    require to != from;
    require idToCheck1 != idToCheck2 && idToCheck3 != idToCheck2 && idToCheck1 != idToCheck3;

    require ids.length == 3;
    require amounts.length == 3;
    require ids[0] == idToCheck1; require amounts[0] == amountToCheck1;
    require ids[1] == idToCheck2; require amounts[1] == amountToCheck2;
    require ids[2] == idToCheck3; require amounts[2] == amountToCheck3;

    uint256 fromBalanceBefore1 = balanceOf(from, idToCheck1);
    uint256 fromBalanceBefore2 = balanceOf(from, idToCheck2);
    uint256 fromBalanceBefore3 = balanceOf(from, idToCheck3);

    uint256 toBalanceBefore1 = balanceOf(to, idToCheck1);
    uint256 toBalanceBefore2 = balanceOf(to, idToCheck2);
    uint256 toBalanceBefore3 = balanceOf(to, idToCheck3);

    safeBatchTransferFrom(e, from, to, ids, amounts, data);

    uint256 fromBalanceAfter1 = balanceOf(from, idToCheck1);
    uint256 fromBalanceAfter2 = balanceOf(from, idToCheck2);
    uint256 fromBalanceAfter3 = balanceOf(from, idToCheck3);

    uint256 toBalanceAfter1 = balanceOf(to, idToCheck1);
    uint256 toBalanceAfter2 = balanceOf(to, idToCheck2);
    uint256 toBalanceAfter3 = balanceOf(to, idToCheck3);

    assert (fromBalanceBefore1 == fromBalanceAfter1 + amountToCheck1)
                && (fromBalanceBefore2 == fromBalanceAfter2 + amountToCheck2)
                && (fromBalanceBefore3 == fromBalanceAfter3 + amountToCheck3), "Something wet wrong";
    assert (toBalanceBefore1 == toBalanceAfter1 - amountToCheck1)
                && (toBalanceBefore2 == toBalanceAfter2 - amountToCheck2)
                && (toBalanceBefore3 == toBalanceAfter3 - amountToCheck3), "Something wet wrong";
}


// STATUS - verified
// cannot transfer more than `from` balance (safeTransferFrom version)
rule cannotTransferMoreSingle(env e){
    address from; address to; uint256 id; uint256 amount; bytes data;
    uint256 balanceBefore = balanceOf(from, id);

    safeTransferFrom@withrevert(e, from, to, id, amount, data);

    assert amount > balanceBefore => lastReverted, "Achtung! Scammer!";
}


// STATUS - verified
// cannot transfer more than allowed (safeBatchTransferFrom version)
rule cannotTransferMoreBatch(env e){
    address from; address to; uint256[] ids; uint256[] amounts; bytes data;
    uint256 idToCheck1; uint256 amountToCheck1;
    uint256 idToCheck2; uint256 amountToCheck2;
    uint256 idToCheck3; uint256 amountToCheck3;

    uint256 balanceBefore1 = balanceOf(from, idToCheck1);
    uint256 balanceBefore2 = balanceOf(from, idToCheck2);
    uint256 balanceBefore3 = balanceOf(from, idToCheck3);

    require ids.length == 3;
    require amounts.length == 3;
    require ids[0] == idToCheck1; require amounts[0] == amountToCheck1;
    require ids[1] == idToCheck2; require amounts[1] == amountToCheck2;
    require ids[2] == idToCheck3; require amounts[2] == amountToCheck3;

    safeBatchTransferFrom@withrevert(e, from, to, ids, amounts, data);

    assert (amountToCheck1 > balanceBefore1 || amountToCheck2 > balanceBefore2 || amountToCheck3 > balanceBefore3) => lastReverted, "Achtung! Scammer!";
}


// STATUS - verified
// Sender calling safeTransferFrom should only reduce 'from' balance and not other's if sending amount is greater than 0
rule transferBalanceReduceEffect(env e){
    address from; address to; address other;
    uint256 id; uint256 amount;
    bytes data;

    require other != to;

    uint256 otherBalanceBefore = balanceOf(other, id);

    safeTransferFrom(e, from, to, id, amount, data);

    uint256 otherBalanceAfter = balanceOf(other, id);

    assert from != other => otherBalanceBefore == otherBalanceAfter, "Don't touch my money!";
}


// STATUS - verified
// Sender calling safeTransferFrom should only increase 'to' balance and not other's if sending amount is greater than 0
rule transferBalanceIncreaseEffect(env e){
    address from; address to; address other;
    uint256 id; uint256 amount;
    bytes data;

    require from != other;

    uint256 otherBalanceBefore = balanceOf(other, id);

    safeTransferFrom(e, from, to, id, amount, data);

    uint256 otherBalanceAfter = balanceOf(other, id);

    assert other != to => otherBalanceBefore == otherBalanceAfter, "Don't touch my money!";
}


// STATUS - verified
// Sender calling safeTransferFrom should only reduce 'from' balance and not other's if sending amount is greater than 0
rule transferBatchBalanceFromEffect(env e){
    address from; address to; address other;
    uint256[] ids; uint256[] amounts;
    uint256 id1; uint256 amount1; uint256 id2; uint256 amount2; uint256 id3; uint256 amount3;
    bytes data;

    require other != to;

    uint256 otherBalanceBefore1 = balanceOf(other, id1);
    uint256 otherBalanceBefore2 = balanceOf(other, id2);
    uint256 otherBalanceBefore3 = balanceOf(other, id3);

    safeBatchTransferFrom(e, from, to, ids, amounts, data);

    uint256 otherBalanceAfter1 = balanceOf(other, id1);
    uint256 otherBalanceAfter2 = balanceOf(other, id2);
    uint256 otherBalanceAfter3 = balanceOf(other, id3);

    assert from != other => (otherBalanceBefore1 == otherBalanceAfter1
                                && otherBalanceBefore2 == otherBalanceAfter2
                                && otherBalanceBefore3 == otherBalanceAfter3), "Don't touch my money!";
}


// STATUS - verified
// Sender calling safeBatchTransferFrom should only increase 'to' balance and not other's if sending amount is greater than 0
rule transferBatchBalanceToEffect(env e){
    address from; address to; address other;
    uint256[] ids; uint256[] amounts;
    uint256 id1; uint256 amount1; uint256 id2; uint256 amount2; uint256 id3; uint256 amount3;
    bytes data;

    require other != from;

    uint256 otherBalanceBefore1 = balanceOf(other, id1);
    uint256 otherBalanceBefore2 = balanceOf(other, id2);
    uint256 otherBalanceBefore3 = balanceOf(other, id3);

    safeBatchTransferFrom(e, from, to, ids, amounts, data);

    uint256 otherBalanceAfter1 = balanceOf(other, id1);
    uint256 otherBalanceAfter2 = balanceOf(other, id2);
    uint256 otherBalanceAfter3 = balanceOf(other, id3);

    assert other != to => (otherBalanceBefore1 == otherBalanceAfter1
                                && otherBalanceBefore2 == otherBalanceAfter2
                                && otherBalanceBefore3 == otherBalanceAfter3), "Don't touch my money!";
}


// STATUS - verified
// cannot transfer without approval (safeTransferFrom version)
rule noTransferForNotApproved(env e) {
    address from; address operator;
    address to; uint256 id; uint256 amount; bytes data;

    require from != e.msg.sender;

    bool approve = isApprovedForAll(from, e.msg.sender);

    safeTransferFrom@withrevert(e, from, to, id, amount, data);

    assert !approve => lastReverted, "You don't have king's approval!";
}


// STATUS - verified
// cannot transfer without approval (safeBatchTransferFrom version)
rule noTransferBatchForNotApproved(env e) {
    address from; address operator; address to;
    bytes data;
    uint256[] ids; uint256[] amounts;

    require from != e.msg.sender;

    bool approve = isApprovedForAll(from, e.msg.sender);

    safeBatchTransferFrom@withrevert(e, from, to, ids, amounts, data);

    assert !approve => lastReverted, "You don't have king's approval!";
}


// STATUS - verified
// safeTransferFrom doesn't affect any approval
rule noTransferEffectOnApproval(env e){
    address from; address to;
    address owner; address operator;
    uint256 id; uint256 amount;
    bytes data;

    bool approveBefore = isApprovedForAll(owner, operator);

    safeTransferFrom(e, from, to, id, amount, data);

    bool approveAfter = isApprovedForAll(owner, operator);

    assert approveBefore == approveAfter, "Something was effected";
}


// STATUS - verified
// safeTransferFrom doesn't affect any approval
rule noTransferBatchEffectOnApproval(env e){
    address from; address to;
    address owner; address operator;
    uint256[] ids; uint256[] amounts;
    bytes data;

    bool approveBefore = isApprovedForAll(owner, operator);

    safeBatchTransferFrom(e, from, to, ids, amounts, data);

    bool approveAfter = isApprovedForAll(owner, operator);

    assert approveBefore == approveAfter, "Something was effected";
}



/////////////////////////////////////////////////
// Mint (7/9)
/////////////////////////////////////////////////


// STATUS - verified
// Additivity of mint: mint(a); mint(b) has same effect as mint(a+b)
rule mintAdditivity(env e){
    address to; uint256 id; uint256 amount; uint256 amount1; uint256 amount2; bytes data;
    require amount == amount1 + amount2;

    storage initialStorage = lastStorage;

    mint(e, to, id, amount, data);

    uint256 balanceAfterSingleTransaction = balanceOf(to, id);

    mint(e, to, id, amount1, data) at initialStorage;
    mint(e, to, id, amount2, data);

    uint256 balanceAfterDoubleTransaction = balanceOf(to, id);

    assert balanceAfterSingleTransaction == balanceAfterDoubleTransaction, "Not additive";
}


// STATUS - verified
// Check that `mint()` revertes in planned scenario(s) (only if `to` is 0)
rule mintRevertCases(env e){
    address to; uint256 id; uint256 amount; bytes data;

    mint@withrevert(e, to, id, amount, data);

    assert to == 0 => lastReverted, "Should revert";
}


// STATUS - verified
// Check that `mintBatch()` revertes in planned scenario(s) (only if `to` is 0 or arrays have different length)
rule mintBatchRevertCases(env e){
    address to; uint256[] ids; uint256[] amounts; bytes data;

    require ids.length < 1000000000;
    require amounts.length < 1000000000;

    mintBatch@withrevert(e, to, ids, amounts, data);

    assert (ids.length != amounts.length || to == 0) => lastReverted, "Should revert";
}


// STATUS - verified
// Check that mint updates `to` balance correctly
rule mintCorrectWork(env e){
    address to; uint256 id; uint256 amount; bytes data;

    uint256 otherBalanceBefore = balanceOf(to, id);

    mint(e, to, id, amount, data);

    uint256 otherBalanceAfter = balanceOf(to, id);

    assert otherBalanceBefore == otherBalanceAfter - amount, "Something is wrong";
}


// STATUS - verified
// check that mintBatch updates `bootcamp participantsfrom` balance correctly
rule mintBatchCorrectWork(env e){
    address to;
    uint256 id1; uint256 id2; uint256 id3;
    uint256 amount1; uint256 amount2; uint256 amount3;
    uint256[] ids; uint256[] amounts;
    bytes data;

    require ids.length == 3;
    require amounts.length == 3;

    require id1 != id2 && id2 != id3 && id3 != id1;
    require ids[0] == id1; require ids[1] == id2; require ids[2] == id3;
    require amounts[0] == amount1; require amounts[1] == amount2; require amounts[2] == amount3;

    uint256 otherBalanceBefore1 = balanceOf(to, id1);
    uint256 otherBalanceBefore2 = balanceOf(to, id2);
    uint256 otherBalanceBefore3 = balanceOf(to, id3);

    mintBatch(e, to, ids, amounts, data);

    uint256 otherBalanceAfter1 = balanceOf(to, id1);
    uint256 otherBalanceAfter2 = balanceOf(to, id2);
    uint256 otherBalanceAfter3 = balanceOf(to, id3);

    assert otherBalanceBefore1 == otherBalanceAfter1 - amount1
            && otherBalanceBefore2 == otherBalanceAfter2 - amount2
            && otherBalanceBefore3 == otherBalanceAfter3 - amount3
            , "Something is wrong";
}


// STATUS - verified
// The user cannot mint more than max_uint256
rule cantMintMoreSingle(env e){
    address to; uint256 id; uint256 amount; bytes data;

    require to_mathint(balanceOf(to, id) + amount) > max_uint256;

    mint@withrevert(e, to, id, amount, data);

    assert lastReverted, "Don't be too greedy!";
}


// STATUS - verified
// the user cannot mint more than max_uint256 (batch version)
rule cantMintMoreBatch(env e){
    address to; bytes data;
    uint256 id1; uint256 id2; uint256 id3;
    uint256 amount1; uint256 amount2; uint256 amount3;
    uint256[] ids; uint256[] amounts;

    require ids.length == 3;
    require amounts.length == 3;

    require ids[0] == id1; require ids[1] == id2; require ids[2] == id3;
    require amounts[0] == amount1; require amounts[1] == amount2; require amounts[2] == amount3;

    require to_mathint(balanceOf(to, id1) + amount1) > max_uint256
                || to_mathint(balanceOf(to, id2) + amount2) > max_uint256
                || to_mathint(balanceOf(to, id3) + amount3) > max_uint256;

    mintBatch@withrevert(e, to, ids, amounts, data);

    assert lastReverted, "Don't be too greedy!";
}


// STATUS - verified
// `mint()` changes only `to` balance
rule cantMintOtherBalances(env e){
    address to; uint256 id; uint256 amount; bytes data;
    address other;

    uint256 otherBalanceBefore = balanceOf(other, id);

    mint(e, to, id, amount, data);

    uint256 otherBalanceAfter = balanceOf(other, id);

    assert other != to => otherBalanceBefore == otherBalanceAfter, "I like to see your money disappearing";
}


// STATUS - verified
// mintBatch changes only `to` balance
rule cantMintBatchOtherBalances(env e){
    address to;
    uint256 id1; uint256 id2; uint256 id3;
    uint256[] ids; uint256[] amounts;
    address other;
    bytes data;

    uint256 otherBalanceBefore1 = balanceOf(other, id1);
    uint256 otherBalanceBefore2 = balanceOf(other, id2);
    uint256 otherBalanceBefore3 = balanceOf(other, id3);

    mintBatch(e, to, ids, amounts, data);

    uint256 otherBalanceAfter1 = balanceOf(other, id1);
    uint256 otherBalanceAfter2 = balanceOf(other, id2);
    uint256 otherBalanceAfter3 = balanceOf(other, id3);

    assert other != to => (otherBalanceBefore1 == otherBalanceAfter1
                                && otherBalanceBefore2 == otherBalanceAfter2
                                && otherBalanceBefore3 == otherBalanceAfter3)
                                , "I like to see your money disappearing";
}


/////////////////////////////////////////////////
// Burn (9/9)
/////////////////////////////////////////////////


// STATUS - verified
// Additivity of burn: burn(a); burn(b) has same effect as burn(a+b)
rule burnAdditivity(env e){
    address from; uint256 id; uint256 amount; uint256 amount1; uint256 amount2;
    require amount == amount1 + amount2;

    storage initialStorage = lastStorage;

    burn(e, from, id, amount);

    uint256 balanceAfterSingleTransaction = balanceOf(from, id);

    burn(e, from, id, amount1) at initialStorage;
    burn(e, from, id, amount2);

    uint256 balanceAfterDoubleTransaction = balanceOf(from, id);

    assert balanceAfterSingleTransaction == balanceAfterDoubleTransaction, "Not additive";
}


// STATUS - verified
// Check that `burn()` revertes in planned scenario(s) (if `from` is 0)
rule burnRevertCases(env e){
    address from; uint256 id; uint256 amount;

    burn@withrevert(e, from, id, amount);

    assert from == 0 => lastReverted, "Should revert";
}


// STATUS - verified
// Check that `balanceOf()` revertes in planned scenario(s) (if `from` is 0 or arrays have different length)
rule burnBatchRevertCases(env e){
    address from; uint256[] ids; uint256[] amounts;

    require ids.length < 1000000000;
    require amounts.length < 1000000000;

    burnBatch@withrevert(e, from, ids, amounts);

    assert (from == 0 || ids.length != amounts.length) => lastReverted, "Should revert";
}


// STATUS - verified
// check that burn updates `from` balance correctly
rule burnCorrectWork(env e){
    address from; uint256 id; uint256 amount;

    uint256 otherBalanceBefore = balanceOf(from, id);

    burn(e, from, id, amount);

    uint256 otherBalanceAfter = balanceOf(from, id);

    assert otherBalanceBefore == otherBalanceAfter + amount, "Something is wrong";
}


// STATUS - verified
// check that burnBatch updates `from` balance correctly
rule burnBatchCorrectWork(env e){
    address from;
    uint256 id1; uint256 id2; uint256 id3;
    uint256 amount1; uint256 amount2; uint256 amount3;
    uint256[] ids; uint256[] amounts;

    require ids.length == 3;

    require id1 != id2 && id2 != id3 && id3 != id1;
    require ids[0] == id1; require ids[1] == id2; require ids[2] == id3;
    require amounts[0] == amount1; require amounts[1] == amount2; require amounts[2] == amount3;

    uint256 otherBalanceBefore1 = balanceOf(from, id1);
    uint256 otherBalanceBefore2 = balanceOf(from, id2);
    uint256 otherBalanceBefore3 = balanceOf(from, id3);

    burnBatch(e, from, ids, amounts);

    uint256 otherBalanceAfter1 = balanceOf(from, id1);
    uint256 otherBalanceAfter2 = balanceOf(from, id2);
    uint256 otherBalanceAfter3 = balanceOf(from, id3);

    assert otherBalanceBefore1 == otherBalanceAfter1 + amount1
            && otherBalanceBefore2 == otherBalanceAfter2 + amount2
            && otherBalanceBefore3 == otherBalanceAfter3 + amount3
            , "Something is wrong";
}


// STATUS - verified
// the user cannot burn more than they have
rule cantBurnMoreSingle(env e){
    address from; uint256 id; uint256 amount;

    require to_mathint(balanceOf(from, id) - amount) < 0;

    burn@withrevert(e, from, id, amount);

    assert lastReverted, "Don't be too greedy!";
}


// STATUS - verified
// the user cannot burn more than they have (batch version)
rule cantBurnMoreBatch(env e){
    address from;
    uint256 id1; uint256 id2; uint256 id3;
    uint256 amount1; uint256 amount2; uint256 amount3;
    uint256[] ids; uint256[] amounts;

    require ids.length == 3;

    require ids[0] == id1; require ids[1] == id2; require ids[2] == id3;
    require amounts[0] == amount1; require amounts[1] == amount2; require amounts[2] == amount3;

    require to_mathint(balanceOf(from, id1) - amount1) < 0
                || to_mathint(balanceOf(from, id2) - amount2) < 0
                || to_mathint(balanceOf(from, id3) - amount3) < 0 ;

    burnBatch@withrevert(e, from, ids, amounts);

    assert lastReverted, "Don't be too greedy!";
}


// STATUS - verified
// burn changes only `from` balance
rule cantBurnOtherBalances(env e){
    address from; uint256 id; uint256 amount;
    address other;

    uint256 otherBalanceBefore = balanceOf(other, id);

    burn(e, from, id, amount);

    uint256 otherBalanceAfter = balanceOf(other, id);

    assert other != from => otherBalanceBefore == otherBalanceAfter, "I like to see your money disappearing";
}


// STATUS - verified
// burnBatch changes only `from` balance
rule cantBurnBatchOtherBalances(env e){
    address from;
    uint256 id1; uint256 id2; uint256 id3;
    uint256 amount1; uint256 amount2; uint256 amount3;
    uint256[] ids; uint256[] amounts;
    address other;

    uint256 otherBalanceBefore1 = balanceOf(other, id1);
    uint256 otherBalanceBefore2 = balanceOf(other, id2);
    uint256 otherBalanceBefore3 = balanceOf(other, id3);

    burnBatch(e, from, ids, amounts);

    uint256 otherBalanceAfter1 = balanceOf(other, id1);
    uint256 otherBalanceAfter2 = balanceOf(other, id2);
    uint256 otherBalanceAfter3 = balanceOf(other, id3);

    assert other != from => (otherBalanceBefore1 == otherBalanceAfter1
                                && otherBalanceBefore2 == otherBalanceAfter2
                                && otherBalanceBefore3 == otherBalanceAfter3)
                                , "I like to see your money disappearing";
}

/////////////////////////////////////////////////
// The rules below were added to this base ERC1155 spec as part of a later
// project with OpenZeppelin covering various ERC1155 extensions.
/////////////////////////////////////////////////

/// The result of transferring a single token must be equivalent whether done
/// via safeTransferFrom or safeBatchTransferFrom.
rule singleTokenSafeTransferFromSafeBatchTransferFromEquivalence {
    storage beforeTransfer = lastStorage;
    env e;

    address holder; address recipient;
    uint256 token; uint256 transferAmount; bytes data;
    uint256[] tokens; uint256[] transferAmounts;

    mathint holderStartingBalance = balanceOf(holder, token);
    mathint recipientStartingBalance = balanceOf(recipient, token);

    require tokens.length == 1; require transferAmounts.length == 1;
    require tokens[0] == token; require transferAmounts[0] == transferAmount;

    // transferring via safeTransferFrom
    safeTransferFrom(e, holder, recipient, token, transferAmount, data) at beforeTransfer;
    mathint holderSafeTransferFromBalanceChange = holderStartingBalance - balanceOf(holder, token);
    mathint recipientSafeTransferFromBalanceChange = balanceOf(recipient, token) - recipientStartingBalance;

    // transferring via safeBatchTransferFrom
    safeBatchTransferFrom(e, holder, recipient, tokens, transferAmounts, data) at beforeTransfer;
    mathint holderSafeBatchTransferFromBalanceChange = holderStartingBalance - balanceOf(holder, token);
    mathint recipientSafeBatchTransferFromBalanceChange = balanceOf(recipient, token) - recipientStartingBalance;

    assert holderSafeTransferFromBalanceChange == holderSafeBatchTransferFromBalanceChange
        && recipientSafeTransferFromBalanceChange == recipientSafeBatchTransferFromBalanceChange,
        "Transferring a single token via safeTransferFrom or safeBatchTransferFrom must be equivalent";
}

/// The results of transferring multiple tokens must be equivalent whether done
/// separately via safeTransferFrom or together via safeBatchTransferFrom.
rule multipleTokenSafeTransferFromSafeBatchTransferFromEquivalence {
    storage beforeTransfers = lastStorage;
    env e;

    address holder; address recipient; bytes data;
    uint256 tokenA; uint256 tokenB; uint256 tokenC;
    uint256 transferAmountA; uint256 transferAmountB; uint256 transferAmountC;
    uint256[] tokens; uint256[] transferAmounts;

    mathint holderStartingBalanceA = balanceOf(holder, tokenA);
    mathint holderStartingBalanceB = balanceOf(holder, tokenB);
    mathint holderStartingBalanceC = balanceOf(holder, tokenC);
    mathint recipientStartingBalanceA = balanceOf(recipient, tokenA);
    mathint recipientStartingBalanceB = balanceOf(recipient, tokenB);
    mathint recipientStartingBalanceC = balanceOf(recipient, tokenC);

    require tokens.length == 3; require transferAmounts.length == 3;
    require tokens[0] == tokenA; require transferAmounts[0] == transferAmountA;
    require tokens[1] == tokenB; require transferAmounts[1] == transferAmountB;
    require tokens[2] == tokenC; require transferAmounts[2] == transferAmountC;

    // transferring via safeTransferFrom
    safeTransferFrom(e, holder, recipient, tokenA, transferAmountA, data) at beforeTransfers;
    safeTransferFrom(e, holder, recipient, tokenB, transferAmountB, data);
    safeTransferFrom(e, holder, recipient, tokenC, transferAmountC, data);
    mathint holderSafeTransferFromBalanceChangeA = holderStartingBalanceA - balanceOf(holder, tokenA);
    mathint holderSafeTransferFromBalanceChangeB = holderStartingBalanceB - balanceOf(holder, tokenB);
    mathint holderSafeTransferFromBalanceChangeC = holderStartingBalanceC - balanceOf(holder, tokenC);
    mathint recipientSafeTransferFromBalanceChangeA = balanceOf(recipient, tokenA) - recipientStartingBalanceA;
    mathint recipientSafeTransferFromBalanceChangeB = balanceOf(recipient, tokenB) - recipientStartingBalanceB;
    mathint recipientSafeTransferFromBalanceChangeC = balanceOf(recipient, tokenC) - recipientStartingBalanceC;

    // transferring via safeBatchTransferFrom
    safeBatchTransferFrom(e, holder, recipient, tokens, transferAmounts, data) at beforeTransfers;
    mathint holderSafeBatchTransferFromBalanceChangeA = holderStartingBalanceA - balanceOf(holder, tokenA);
    mathint holderSafeBatchTransferFromBalanceChangeB = holderStartingBalanceB - balanceOf(holder, tokenB);
    mathint holderSafeBatchTransferFromBalanceChangeC = holderStartingBalanceC - balanceOf(holder, tokenC);
    mathint recipientSafeBatchTransferFromBalanceChangeA = balanceOf(recipient, tokenA) - recipientStartingBalanceA;
    mathint recipientSafeBatchTransferFromBalanceChangeB = balanceOf(recipient, tokenB) - recipientStartingBalanceB;
    mathint recipientSafeBatchTransferFromBalanceChangeC = balanceOf(recipient, tokenC) - recipientStartingBalanceC;

    assert holderSafeTransferFromBalanceChangeA == holderSafeBatchTransferFromBalanceChangeA
        && holderSafeTransferFromBalanceChangeB == holderSafeBatchTransferFromBalanceChangeB
        && holderSafeTransferFromBalanceChangeC == holderSafeBatchTransferFromBalanceChangeC
        && recipientSafeTransferFromBalanceChangeA == recipientSafeBatchTransferFromBalanceChangeA
        && recipientSafeTransferFromBalanceChangeB == recipientSafeBatchTransferFromBalanceChangeB
        && recipientSafeTransferFromBalanceChangeC == recipientSafeBatchTransferFromBalanceChangeC,
        "Transferring multiple tokens via safeTransferFrom or safeBatchTransferFrom must be equivalent";
}

/// If transfer methods do not revert, the input arrays must be the same length.
rule transfersHaveSameLengthInputArrays {
    env e;

    address recipient; bytes data;
    uint256[] tokens; uint256[] transferAmounts;
    uint max_int = 0xffffffffffffffffffffffffffffffff;

    require tokens.length >= 0 && tokens.length <= max_int;
    require transferAmounts.length >= 0 && transferAmounts.length <= max_int;

    safeBatchTransferFrom(e, _, recipient, tokens, transferAmounts, data);

    uint256 tokensLength = tokens.length;
    uint256 transferAmountsLength = transferAmounts.length;

    assert tokens.length == transferAmounts.length,
        "If transfer methods do not revert, the input arrays must be the same length";
}