vacp2p/staking-reward-streamer
1
0
Fork 0
mirror of https://github.com/vacp2p/staking-reward-streamer.git synced 2026-01-09 21:18:01 -05:00
Code Issues Packages Projects Releases Wiki Activity

WIP

Browse Source
This commit is contained in:
r4bbit
2024-10-17 13:27:02 +02:00
parent 2ee6eb8065
commit 29f051bb16
1 changed files with 56 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

56
certora/specs/RewardsStreamerMP.spec
View File

@@ -3,7 +3,11 @@ using ERC20A as staked;
methods {
function totalStaked() external returns (uint256) envfree;
function totalMP() external returns (uint256) envfree;
function users(address) external returns (uint256, uint256, uint256, uint256, uint256, uint256) envfree;
function lastMPUpdatedTime() external returns (uint256) envfree;
function updateGlobalState() external;
function updateUserMP(address userAddress) external;
}
ghost mathint sumOfBalances {
@@ -14,6 +18,22 @@ hook Sstore users[KEY address account].stakedBalance uint256 newValue (uint256 o
sumOfBalances = sumOfBalances - oldValue + newValue;
}
hook Sload uint256 balance users[KEY address addr].stakedBalance {
require sumOfBalances >= to_mathint(balance);
}
ghost mathint sumOfAccountMP {
init_state axiom sumOfAccountMP == 0;
}
hook Sstore users[KEY address account].userMP uint256 newValue (uint256 oldValue) {
sumOfAccountMP = sumOfAccountMP - oldValue + newValue;
}
hook Sload uint256 userMP users[KEY address addr].userMP {
require sumOfAccountMP >= to_mathint(userMP);
}
function getAccountMaxMP(address account) returns uint256 {
uint256 maxMP;
_, _, _, maxMP, _, _ = streamer.users(account);
@@ -41,3 +61,39 @@ invariant accountMPLessEqualAccountMaxMP(address account)
invariant accountMPGreaterEqualAccountStakedBalance(address account)
to_mathint(getAccountMP(account)) >= to_mathint(getAccountStakedBalance(account));
invariant totalMPGreaterEqualSumOfAccountMP()
to_mathint(totalMP()) >= sumOfAccountMP
{ preserved with (env e) {
requireInvariant sumOfBalancesIsTotalStaked();
requireInvariant accountMPGreaterEqualAccountStakedBalance(e.msg.sender);
//requireInvariant accountMPLessEqualAccountMaxMP(e.msg.sender);
}}
// rule sumOfAccountMPIsTotalMP() {
//
// method f;
// calldataarg args;
// env e;
//
// requireInvariant accountMPGreaterEqualAccountStakedBalance(e.msg.sender);
// requireInvariant accountMPLessEqualAccountMaxMP(e.msg.sender);
//
// uint256 t = lastMPUpdatedTime(); // 10
//
// updateGlobalState(e);
// updateUserMP(e, args);
//
// require sumOfAccountMP == to_mathint(totalMP());
//
// require lastMPUpdatedTime() == t; // 10
// f(e, args); // stake
// require lastMPUpdatedTime() == t; // 10
//
// updateGlobalState(e);
// updateUserMP(e, args);
// require lastMPUpdatedTime() == t;
//
//
// assert sumOfAccountMP == to_mathint(totalMP());
// }