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

WIP

This commit is contained in:
r4bbit 2024-07-30 14:54:44 +02:00
parent 60d80bf4b2
commit de3790e0fc
No known key found for this signature in database
GPG Key ID: E95F1E9447DC91A9
3 changed files with 30 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
certora/confs/StakeManager.conf
View File

@ -1,5 +1,5 @@
{
"files":
"files":
["contracts/StakeManager.sol",
"certora/helpers/ERC20A.sol"
],
@ -12,6 +12,7 @@
"optimistic_loop": true,
"loop_iter": "3",
"packages": [
"forge-std=lib/forge-std/src",
"@openzeppelin=lib/openzeppelin-contracts"
]
}

10
certora/specs/StakeManager.spec
View File

@ -7,7 +7,7 @@ methods {
function _.migrateFrom(address, bool, StakeManager.Account) external => NONDET;
function _.increaseTotalMP(uint256) external => NONDET;
function _.migrationInitialize(uint256,uint256,uint256,uint256) external => NONDET;
function accounts(address) external returns(address, uint256, uint256, uint256, uint256, uint256, uint256) envfree;
function accounts(address) external returns(address, uint256, uint256, uint256, uint256, uint256, uint256, uint256) envfree;
function Math.mulDiv(uint256 a, uint256 b, uint256 c) internal returns uint256 => mulDivSummary(a,b,c);
}
@ -18,28 +18,28 @@ function mulDivSummary(uint256 a, uint256 b, uint256 c) returns uint256 {
function getAccountBalance(address addr) returns uint256 {
uint256 balance;
_, balance, _, _, _, _, _ = accounts(addr);
_, balance, _, _, _, _, _, _ = accounts(addr);
return balance;
}
function getAccountBonusMultiplierPoints(address addr) returns uint256 {
uint256 bonusMP;
_, _, bonusMP, _, _, _, _ = accounts(addr);
_, _, bonusMP, _, _, _, _, _ = accounts(addr);
return bonusMP;
}
function getAccountCurrentMultiplierPoints(address addr) returns uint256 {
uint256 totalMP;
_, _, _, totalMP, _, _, _ = accounts(addr);
_, _, _, totalMP, _, _, _, _ = accounts(addr);
return totalMP;
}
function getAccountLockUntil(address addr) returns uint256 {
uint256 lockUntil;
_, _, _, _, _, lockUntil, _ = accounts(addr);
_, _, _, _, _, lockUntil, _, _ = accounts(addr);
return lockUntil;
}

25
certora/specs/StakeManagerProcessAccount.spec
View File

@ -2,10 +2,11 @@ using ERC20A as staked;
methods {
function staked.balanceOf(address) external returns (uint256) envfree;
function totalSupplyBalance() external returns (uint256) envfree;
function accounts(address) external returns(address, uint256, uint256, uint256, uint256, uint256, uint256) envfree;
function accounts(address) external returns(address, uint256, uint256, uint256, uint256, uint256, uint256, uint256) envfree;
function _processAccount(StakeManager.Account storage account, uint256 _limitEpoch) internal with(env e) => markAccountProccessed(e.msg.sender, _limitEpoch);
function _.migrationInitialize(uint256,uint256,uint256,uint256) external => NONDET;
function pendingMPToBeMinted() external returns (uint256) envfree;
}
// keeps track of the last epoch an account was processed
@ -19,7 +20,7 @@ function markAccountProccessed(address account, uint256 _limitEpoch) {
function getAccountLockUntil(address addr) returns uint256 {
uint256 lockUntil;
_, _, _, _, _, lockUntil, _ = accounts(addr);
_, _, _, _, _, lockUntil, _, _ = accounts(addr);
return lockUntil;
}
@ -69,6 +70,26 @@ rule checkAccountProcessedBeforeStoring(method f) filtered {
}
rule pendingMPToMintShouldNotBeBiggerTotalSupplyMP(method f) filtered {
f -> !requiresPreviousManager(f) && !requiresNextManager(f)
} {
calldataarg args;
env e;
address account;
address account2;
mathint amount;
uint256 pendingMPBefore = currentContract.pendingMPToBeMinted();
currentContract.stake(e, amount, 0);
uint256 pendingMPAfter = currentContract.pendingMPToBeMinted();
require e.block.timestamp > currentContract.currentEpoch()
currentContract.executeAccount(account1)
assert pendingMPAfter > pendingMPBefore;
}
/*
Below is a rule that finds all methods that change an account's balance.
This is just for debugging purposes and not meant to be a production rule.