From 3fec9631ae29ab7a328b01a43ac6d3e91e0517e9 Mon Sep 17 00:00:00 2001 From: r4bbit <445106+0x-r4bbit@users.noreply.github.com> Date: Mon, 18 Mar 2024 12:12:02 +0100 Subject: [PATCH] chore(certora): upgrade certora to 7.0.7 This upgrade certora-cli on CI to version 7.0.7 which no longer requires the usage of the `STORAGE` keyword in storage hooks. --- .github/workflows/test.yml | 2 +- certora/specs/CommunityERC721.spec | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) 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); }