From 428197be69e39bd1169d73541134902253c12b83 Mon Sep 17 00:00:00 2001 From: Thomas Adams Date: Thu, 26 May 2022 11:20:46 -0700 Subject: [PATCH] Added tester rule for only burn --- certora/specs/ERC1155Burnable.spec | 23 ++++++++++++++++++++++- 1 file changed, 22 insertions(+), 1 deletion(-) diff --git a/certora/specs/ERC1155Burnable.spec b/certora/specs/ERC1155Burnable.spec index 3e67c1919..344d25380 100644 --- a/certora/specs/ERC1155Burnable.spec +++ b/certora/specs/ERC1155Burnable.spec @@ -1,7 +1,28 @@ +methods { + balanceOf(address, uint256) returns uint256 envfree + isApprovedForAll(address,address) returns bool envfree +} + +/// If a method call reduces account balances, the caller should be either the +/// owner of the account or approved by the owner to act on its behalf. +rule onlyApprovedCanReduceBalance { + address holder; uint256 token; uint256 amount; + uint256 balanceBefore = balanceOf(holder, token); + + env e; + burn(e, holder, token, amount); // TODO Replace burn with appropriate general function + + uint256 balanceAfter = balanceOf(holder, token); + + assert balanceAfter < balanceBefore => e.msg.sender == holder || isApprovedForAll(holder, e.msg.sender); +} + +/// This rule should always fail. rule sanity { method f; env e; calldataarg args; f(e, args); - assert false; + assert false, + "This rule should always fail"; } \ No newline at end of file