chore(StakeManager.spec): add invariant sumOfMultiplierPoints

This commit is contained in:
r4bbit 2024-02-07 14:02:48 +01:00
parent a0585d98e2
commit c05dff9b6c
No known key found for this signature in database
GPG Key ID: E95F1E9447DC91A9
2 changed files with 26 additions and 2 deletions

View File

@ -1,7 +1,11 @@
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 stakeSupply() external returns (uint256) envfree;
function multiplierSupply() external returns (uint256) envfree;
function oldManager() external returns (address) envfree;
function _.migrate(address, StakeManager.Account) external => NONDET;
} }
function isMigrationfunction(method f) returns bool { function isMigrationfunction(method f) returns bool {
@ -12,21 +16,38 @@ function isMigrationfunction(method f) returns bool {
/* assume that migration is zero, causing the verification to take into account only /* assume that migration is zero, causing the verification to take into account only
cases where it is zero. specifically no externall call to the migration contract */ cases where it is zero. specifically no externall call to the migration contract */
function simplification() { function simplification(env e) {
require e.msg.sender != 0;
require currentContract.oldManager() == 0;
require currentContract.migration == 0; require currentContract.migration == 0;
} }
ghost mathint sumOfBalances /* sigma account[u].balance forall u */ { ghost mathint sumOfBalances { /* sigma account[u].balance forall u */
init_state axiom sumOfBalances == 0; init_state axiom sumOfBalances == 0;
} }
ghost mathint sumOfMultipliers /* sigma account[u].multiplier forall u */
{
init_state axiom sumOfMultipliers == 0;
}
hook Sstore accounts[KEY address addr].balance uint256 newValue (uint256 oldValue) STORAGE { hook Sstore accounts[KEY address addr].balance uint256 newValue (uint256 oldValue) STORAGE {
sumOfBalances = sumOfBalances - oldValue + newValue; sumOfBalances = sumOfBalances - oldValue + newValue;
} }
hook Sstore accounts[KEY address addr].multiplier uint256 newValue (uint256 oldValue) STORAGE {
sumOfMultipliers = sumOfMultipliers - oldValue + newValue;
}
invariant sumOfBalancesIsStakeSupply() invariant sumOfBalancesIsStakeSupply()
sumOfBalances == to_mathint(stakeSupply()); sumOfBalances == to_mathint(stakeSupply());
invariant sumOfMultipliersIsMultiplierSupply()
sumOfMultipliers == to_mathint(multiplierSupply())
{ preserved with (env e) {
simplification(e);
}
}
rule reachability(method f) rule reachability(method f)
{ {

View File

@ -165,7 +165,10 @@ contract StakeManager is Ownable {
Account storage account = accounts[msg.sender]; Account storage account = accounts[msg.sender];
stakedToken.approve(address(migration), account.balance); stakedToken.approve(address(migration), account.balance);
migration.migrate(msg.sender, account); migration.migrate(msg.sender, account);
multiplierSupply -= accounts[msg.sender].multiplier;
delete accounts[msg.sender]; delete accounts[msg.sender];
return migration; return migration;
} }