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

chore: add cerora rules for `stakeSupply` ghost rule

This commit is contained in:
Nurit Dor 2024-01-24 12:16:01 +01:00 committed by r4bbit
parent 4f2f6d3a75
commit a0585d98e2
No known key found for this signature in database
GPG Key ID: E95F1E9447DC91A9
1 changed files with 12 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
certora/specs/StakeManager.spec
View File

@ -1,6 +1,7 @@
using ERC20A as staked; using ERC20A as staked;
methods { methods {
function staked.balanceOf(address) external returns (uint256) envfree; function staked.balanceOf(address) external returns (uint256) envfree;
function stakeSupply() external returns (uint256) envfree;
} }
function isMigrationfunction(method f) returns bool { function isMigrationfunction(method f) returns bool {
@ -15,6 +16,17 @@ function simplification() {
require currentContract.migration == 0; require currentContract.migration == 0;
} }
ghost mathint sumOfBalances /* sigma account[u].balance forall u */ {
init_state axiom sumOfBalances == 0;
}
hook Sstore accounts[KEY address addr].balance uint256 newValue (uint256 oldValue) STORAGE {
sumOfBalances = sumOfBalances - oldValue + newValue;
}
invariant sumOfBalancesIsStakeSupply()
sumOfBalances == to_mathint(stakeSupply());
rule reachability(method f) rule reachability(method f)
{ {