diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 85be65e..755b507 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -135,7 +135,7 @@ jobs: with: { java-version: "11", java-package: jre } - name: Install Certora CLI - run: pip3 install certora-cli==6.3.1 + run: pip3 install certora-cli==7.0.7 - name: Install Solidity run: | diff --git a/certora/specs/CommunityERC721.spec b/certora/specs/CommunityERC721.spec index e2df7d2..f782f94 100644 --- a/certora/specs/CommunityERC721.spec +++ b/certora/specs/CommunityERC721.spec @@ -16,11 +16,11 @@ ghost mathint sumOfBalances { init_state axiom sumOfBalances == 0; } -hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE { +hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) { sumOfBalances = sumOfBalances - oldValue + newValue; } -hook Sload uint256 balance _balances[KEY address addr] STORAGE { +hook Sload uint256 balance _balances[KEY address addr] { require sumOfBalances >= to_mathint(balance); }