From 4dc0ff9fe3aa4ff2672f0de052a9e966afe13f55 Mon Sep 17 00:00:00 2001 From: Thomas Adams Date: Thu, 26 May 2022 14:35:27 -0700 Subject: [PATCH] Added assert message --- certora/specs/ERC1155Burnable.spec | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/certora/specs/ERC1155Burnable.spec b/certora/specs/ERC1155Burnable.spec index d38731079..60418bbbf 100644 --- a/certora/specs/ERC1155Burnable.spec +++ b/certora/specs/ERC1155Burnable.spec @@ -3,9 +3,9 @@ methods { 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 { +/// If a method call reduces account balances, the caller must be either the +/// owner of the account or approved by the owner to act on the owner's behalf. +rule onlyHolderOrApprovedCanReduceBalance { address holder; uint256 token; uint256 amount; uint256 balanceBefore = balanceOf(holder, token); @@ -14,7 +14,8 @@ rule onlyApprovedCanReduceBalance { uint256 balanceAfter = balanceOf(holder, token); - assert balanceAfter < balanceBefore => e.msg.sender == holder || isApprovedForAll(holder, e.msg.sender); // TODO add assert message + assert balanceAfter < balanceBefore => e.msg.sender == holder || isApprovedForAll(holder, e.msg.sender), + "An account balance may only be reduced by the holder or a holder-approved agent"; } /// This rule should always fail.