diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 3cf3d04..f36fedc 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -136,7 +136,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/StakeManager.spec b/certora/specs/StakeManager.spec index 62102d7..79f41c0 100644 --- a/certora/specs/StakeManager.spec +++ b/certora/specs/StakeManager.spec @@ -83,15 +83,15 @@ ghost mathint sumOfBalances /* sigma account[u].balance forall u */ { init_state axiom sumOfBalances == 0; } -hook Sstore epochs[KEY uint256 epochId].epochReward uint256 newValue (uint256 oldValue) STORAGE { +hook Sstore epochs[KEY uint256 epochId].epochReward uint256 newValue (uint256 oldValue) { sumOfEpochRewards = sumOfEpochRewards - oldValue + newValue; } -hook Sstore accounts[KEY address addr].balance uint256 newValue (uint256 oldValue) STORAGE { +hook Sstore accounts[KEY address addr].balance uint256 newValue (uint256 oldValue) { sumOfBalances = sumOfBalances - oldValue + newValue; } -hook Sstore accounts[KEY address addr].currentMP uint256 newValue (uint256 oldValue) STORAGE { +hook Sstore accounts[KEY address addr].currentMP uint256 newValue (uint256 oldValue) { sumOfMultipliers = sumOfMultipliers - oldValue + newValue; } diff --git a/certora/specs/StakeManagerProcessAccount.spec b/certora/specs/StakeManagerProcessAccount.spec index ea129fd..d2da58a 100644 --- a/certora/specs/StakeManagerProcessAccount.spec +++ b/certora/specs/StakeManagerProcessAccount.spec @@ -24,7 +24,7 @@ function getAccountLockUntil(address addr) returns uint256 { return lockUntil; } -hook Sstore accounts[KEY address addr].balance uint256 newValue (uint256 oldValue) STORAGE { +hook Sstore accounts[KEY address addr].balance uint256 newValue (uint256 oldValue) { balanceChangedInEpoch[addr] = accountProcessed[addr]; }