From ea2b5a3668ec9e8473b7622592466ec596b9a995 Mon Sep 17 00:00:00 2001 From: FT <140458077+zeevick10@users.noreply.github.com> Date: Wed, 22 Jan 2025 16:45:37 +0100 Subject: [PATCH] fix typo (#5451) --- certora/specs/ERC20FlashMint.spec | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/certora/specs/ERC20FlashMint.spec b/certora/specs/ERC20FlashMint.spec index 4071052ea7f..6942495b0bf 100644 --- a/certora/specs/ERC20FlashMint.spec +++ b/certora/specs/ERC20FlashMint.spec @@ -18,7 +18,7 @@ methods { */ ghost mapping(address => mathint) trackedMintAmount; ghost mapping(address => mathint) trackedBurnAmount; -ghost mapping(address => mapping(address => mathint)) trackedTransferedAmount; +ghost mapping(address => mapping(address => mathint)) trackedTransferredAmount; function specUpdate(address from, address to, uint256 amount) { if (from == 0 && to == 0) { assert(false); } // defensive @@ -28,7 +28,7 @@ function specUpdate(address from, address to, uint256 amount) { } else if (to == 0) { trackedBurnAmount[from] = amount; } else { - trackedTransferedAmount[from][to] = amount; + trackedTransferredAmount[from][to] = amount; } } @@ -51,5 +51,5 @@ rule checkMintAndBurn(env e) { assert trackedMintAmount[receiver] == to_mathint(amount); assert trackedBurnAmount[receiver] == amount + to_mathint(recipient == 0 ? fees : 0); - assert (fees > 0 && recipient != 0) => trackedTransferedAmount[receiver][recipient] == to_mathint(fees); + assert (fees > 0 && recipient != 0) => trackedTransferredAmount[receiver][recipient] == to_mathint(fees); }