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

fix(Certora specs): make specs compile again 

There have been a bunch of breaking changes in the staking contract that
resulted in our specs not compiling.

This commit fixes this, however it does not yet ensure the prover is
satisfied.
This commit is contained in:
r4bbit 2024-03-01 10:35:19 +01:00 committed by Ricardo Guilherme Schmidt
parent d733cc3fd3
commit d7ab130d30
2 changed files with 17 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
certora/specs/StakeManager.spec
View File

@ -1,26 +1,26 @@
using ERC20A as staked;
methods {
function staked.balanceOf(address) external returns (uint256) envfree;
function stakeSupply() external returns (uint256) envfree;
function multiplierSupply() external returns (uint256) envfree;
function totalSupplyBalance() external returns (uint256) envfree;
function totalSupplyMP() external returns (uint256) envfree;
function oldManager() external returns (address) envfree;
function _.migrateFrom(address, bool, StakeManager.Account) external => NONDET;
function _.increaseMPFromMigration(uint256) external => NONDET;
function _.migrationInitialize(uint256,uint256,uint256,uint256) external => NONDET;
function accounts(address) external returns(uint256, uint256, uint256, uint256, uint256, address) envfree;
function accounts(address) external returns(address, uint256, uint256, uint256, uint256, uint256, uint256) envfree;
}
function getAccountMultiplierPoints(address addr) returns uint256 {
uint256 multiplierPoints;
_, _, multiplierPoints, _, _, _ = accounts(addr);
_, _, _, multiplierPoints, _, _, _ = accounts(addr);
return multiplierPoints;
}
function getAccountBalance(address addr) returns uint256 {
uint256 balance;
_, balance, _, _, _, _ = accounts(addr);
_, balance, _, _, _, _, _ = accounts(addr);
return balance;
}
@ -59,17 +59,17 @@ hook Sstore accounts[KEY address addr].balance uint256 newValue (uint256 oldValu
sumOfBalances = sumOfBalances - oldValue + newValue;
}
hook Sstore accounts[KEY address addr].multiplier uint256 newValue (uint256 oldValue) STORAGE {
hook Sstore accounts[KEY address addr].currentMP uint256 newValue (uint256 oldValue) STORAGE {
sumOfMultipliers = sumOfMultipliers - oldValue + newValue;
}
invariant sumOfBalancesIsStakeSupply()
sumOfBalances == to_mathint(stakeSupply());
sumOfBalances == to_mathint(totalSupplyBalance());
invariant sumOfMultipliersIsMultiplierSupply()
sumOfMultipliers == to_mathint(multiplierSupply())
{ preserved with (env e) {
simplification(e);
sumOfMultipliers == to_mathint(totalSupplyMP())
{ preserved with () {
simplification();
}
}

15
certora/specs/StakeManagerStartMigration.spec
View File

@ -3,27 +3,26 @@ using StakeManagerNew as newStakeManager;
methods {
function staked.balanceOf(address) external returns (uint256) envfree;
function stakeSupply() external returns (uint256) envfree;
function multiplierSupply() external returns (uint256) envfree;
function totalSupplyBalance() external returns (uint256) envfree;
function totalSupplyMP() external returns (uint256) envfree;
function oldManager() external returns (address) envfree;
function accounts(address) external returns(uint256, uint256, uint256, uint256, uint256, address) envfree;
function accounts(address) external returns(address, uint256, uint256, uint256, uint256, uint256, uint256) envfree;
function _.migrationInitialize(uint256,uint256,uint256,uint256) external => DISPATCHER(true);
function StakeManagerNew.stakeSupply() external returns (uint256) envfree;
//function _.stakeSupply() external => DISPATCHER(true);
function StakeManagerNew.totalSupplyBalance() external returns (uint256) envfree;
}
function getAccountMultiplierPoints(address addr) returns uint256 {
uint256 multiplierPoints;
_, _, multiplierPoints, _, _, _ = accounts(addr);
_, _, _, multiplierPoints, _, _, _ = accounts(addr);
return multiplierPoints;
}
function getAccountBalance(address addr) returns uint256 {
uint256 balance;
_, balance, _, _, _, _ = accounts(addr);
_, balance, _, _, _, _, _ = accounts(addr);
return balance;
}
@ -101,7 +100,7 @@ rule startMigrationCorrect {
startMigration(e, newContract);
assert currentContract.migration == newContract;
assert newStakeManager.stakeSupply() == currentContract.stakeSupply();
assert newStakeManager.totalSupplyBalance() == currentContract.totalSupplyBalance();
}
rule migrationLockedIn {