logos-co
/
staking
mirror of https://github.com/logos-co/staking.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

chore(certora): upgrade certora-cli to 7.0.7 

This upgrade certora-cli on CI to version 7.0.7 which no longer requires
the `STORAGE` keyword in storage hooks.
This commit is contained in:
r4bbit 2024-03-18 12:08:50 +01:00
parent 70b092ab00
commit 6182d9508c
3 changed files with 5 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
.github/workflows/ci.yml vendored
View File

@ -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: |

6
certora/specs/StakeManager.spec
View File

@ -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;
}

2
certora/specs/StakeManagerProcessAccount.spec
View File

@ -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];
}