From 33e2ff048b06e9f0a3810de001452da6349777c9 Mon Sep 17 00:00:00 2001 From: r4bbit <445106+0x-r4bbit@users.noreply.github.com> Date: Tue, 17 Sep 2024 13:28:57 +0200 Subject: [PATCH] refactor(certora): introduce shared.spec to reuse helper functions We have a couple of helper functions redefined in multiple spec files. This commit introduces a `shared.spec` that provides such functions. The file is then imported in other spec files, so we can make use of the functions there. Closes #87 --- certora/specs/StakeManager.spec | 42 ++----------------- certora/specs/StakeManagerProcessAccount.spec | 21 ++-------- certora/specs/StakeManagerStartMigration.spec | 17 +------- certora/specs/StakeVault.spec | 9 +--- certora/specs/shared.spec | 42 +++++++++++++++++++ 5 files changed, 52 insertions(+), 79 deletions(-) create mode 100644 certora/specs/shared.spec diff --git a/certora/specs/StakeManager.spec b/certora/specs/StakeManager.spec index 81cce58..8b49a56 100644 --- a/certora/specs/StakeManager.spec +++ b/certora/specs/StakeManager.spec @@ -1,4 +1,7 @@ +import "./shared.spec"; + using ERC20A as staked; + methods { function staked.balanceOf(address) external returns (uint256) envfree; function totalSupplyBalance() external returns (uint256) envfree; @@ -17,34 +20,6 @@ function mulDivSummary(uint256 a, uint256 b, uint256 c) returns uint256 { return require_uint256(a*b/c); } -function getAccountBalance(address addr) returns uint256 { - uint256 balance; - _, balance, _, _, _, _, _, _ = accounts(addr); - - return balance; -} - -function getAccountBonusMultiplierPoints(address addr) returns uint256 { - uint256 bonusMP; - _, _, bonusMP, _, _, _, _, _ = accounts(addr); - - return bonusMP; -} - -function getAccountCurrentMultiplierPoints(address addr) returns uint256 { - uint256 totalMP; - _, _, _, totalMP, _, _, _, _ = accounts(addr); - - return totalMP; -} - -function getAccountLockUntil(address addr) returns uint256 { - uint256 lockUntil; - _, _, _, _, _, lockUntil, _, _ = accounts(addr); - - return lockUntil; -} - function isMigrationfunction(method f) returns bool { return f.selector == sig:migrateTo(bool).selector || @@ -59,17 +34,6 @@ function simplification(env e) { require e.msg.sender != 0; } -definition requiresPreviousManager(method f) returns bool = ( - f.selector == sig:migrationInitialize(uint256,uint256,uint256,uint256,uint256,uint256,uint256).selector || - f.selector == sig:migrateFrom(address,bool,StakeManager.Account).selector || - f.selector == sig:increaseTotalMP(uint256).selector - ); - -definition requiresNextManager(method f) returns bool = ( - f.selector == sig:migrateTo(bool).selector || - f.selector == sig:transferNonPending().selector - ); - ghost mathint sumOfEpochRewards { init_state axiom sumOfEpochRewards == 0; diff --git a/certora/specs/StakeManagerProcessAccount.spec b/certora/specs/StakeManagerProcessAccount.spec index c121520..e964acb 100644 --- a/certora/specs/StakeManagerProcessAccount.spec +++ b/certora/specs/StakeManagerProcessAccount.spec @@ -1,4 +1,7 @@ +import "./shared.spec"; + using ERC20A as staked; + methods { function staked.balanceOf(address) external returns (uint256) envfree; function totalSupplyBalance() external returns (uint256) envfree; @@ -20,28 +23,10 @@ function markAccountProccessed(address account, uint256 _limitEpoch) { accountProcessed[account] = to_mathint(_limitEpoch); } -function getAccountLockUntil(address addr) returns uint256 { - uint256 lockUntil; - _, _, _, _, _, lockUntil, _, _ = accounts(addr); - - return lockUntil; -} - hook Sstore accounts[KEY address addr].balance uint256 newValue (uint256 oldValue) { balanceChangedInEpoch[addr] = accountProcessed[addr]; } -definition requiresPreviousManager(method f) returns bool = ( - f.selector == sig:migrationInitialize(uint256,uint256,uint256,uint256,uint256,uint256,uint256).selector || - f.selector == sig:migrateFrom(address,bool,StakeManager.Account).selector || - f.selector == sig:increaseTotalMP(uint256).selector - ); - -definition requiresNextManager(method f) returns bool = ( - f.selector == sig:migrateTo(bool).selector || - f.selector == sig:transferNonPending().selector - ); - /* If a balance of an account has changed, the account should have been processed up to the `currentEpoch`. This is filtering out most of migration related functions, as those will be vacuous. diff --git a/certora/specs/StakeManagerStartMigration.spec b/certora/specs/StakeManagerStartMigration.spec index c469914..c1f36f9 100644 --- a/certora/specs/StakeManagerStartMigration.spec +++ b/certora/specs/StakeManagerStartMigration.spec @@ -1,3 +1,5 @@ +import "./shared.spec"; + using ERC20A as staked; using StakeManagerNew as newStakeManager; @@ -12,21 +14,6 @@ methods { function StakeManagerNew.totalSupplyBalance() external returns (uint256) envfree; } - -function getAccountMultiplierPoints(address addr) returns uint256 { - uint256 multiplierPoints; - _, _, _, multiplierPoints, _, _, _, _ = accounts(addr); - - return multiplierPoints; -} - -function getAccountBalance(address addr) returns uint256 { - uint256 balance; - _, balance, _, _, _, _, _, _ = accounts(addr); - - return balance; -} - definition blockedWhenMigrating(method f) returns bool = ( f.selector == sig:stake(uint256, uint256).selector || f.selector == sig:unstake(uint256).selector || diff --git a/certora/specs/StakeVault.spec b/certora/specs/StakeVault.spec index cadb9c4..c1c02b1 100644 --- a/certora/specs/StakeVault.spec +++ b/certora/specs/StakeVault.spec @@ -1,3 +1,5 @@ +import "./shared.spec"; + using ERC20A as staked; using StakeManager as stakeManager; @@ -17,13 +19,6 @@ function mulDivSummary(uint256 a, uint256 b, uint256 c) returns uint256 { return require_uint256(a*b/c); } -function getAccountBalance(address addr) returns uint256 { - uint256 balance; - _, balance, _, _, _, _, _, _ = stakeManager.accounts(addr); - - return balance; -} - definition isMigrationFunction(method f) returns bool = ( f.selector == sig:stakeManager.migrationInitialize(uint256,uint256,uint256,uint256,uint256,uint256,uint256).selector || f.selector == sig:stakeManager.migrateFrom(address,bool,StakeManager.Account).selector || diff --git a/certora/specs/shared.spec b/certora/specs/shared.spec new file mode 100644 index 0000000..a4731e2 --- /dev/null +++ b/certora/specs/shared.spec @@ -0,0 +1,42 @@ +using StakeManager as _stakeManager; + +definition requiresPreviousManager(method f) returns bool = ( + f.selector == sig:_stakeManager.migrationInitialize(uint256,uint256,uint256,uint256,uint256,uint256,uint256).selector || + f.selector == sig:_stakeManager.migrateFrom(address,bool,StakeManager.Account).selector || + f.selector == sig:_stakeManager.increaseTotalMP(uint256).selector + ); + +definition requiresNextManager(method f) returns bool = ( + f.selector == sig:_stakeManager.migrateTo(bool).selector || + f.selector == sig:_stakeManager.transferNonPending().selector + ); + +function getAccountBalance(address addr) returns uint256 { + uint256 balance; + _, balance, _, _, _, _, _, _ = _stakeManager.accounts(addr); + + return balance; +} + +function getAccountBonusMultiplierPoints(address addr) returns uint256 { + uint256 bonusMP; + _, _, bonusMP, _, _, _, _, _ = _stakeManager.accounts(addr); + + return bonusMP; +} + +function getAccountCurrentMultiplierPoints(address addr) returns uint256 { + uint256 totalMP; + _, _, _, totalMP, _, _, _, _ = _stakeManager.accounts(addr); + + return totalMP; +} + +function getAccountLockUntil(address addr) returns uint256 { + uint256 lockUntil; + _, _, _, _, _, lockUntil, _, _ = _stakeManager.accounts(addr); + + return lockUntil; +} + +