Skip to content

Commit

Permalink
fix(certora/specs): Make rules work again
Browse files Browse the repository at this point in the history
  • Loading branch information
3esmit committed Nov 15, 2024
1 parent 520e4f8 commit 99c73be
Show file tree
Hide file tree
Showing 6 changed files with 44 additions and 18 deletions.
31 changes: 29 additions & 2 deletions certora/specs/MaxMPRule.spec
Original file line number Diff line number Diff line change
@@ -1,15 +1,42 @@
import "./shared.spec";

methods {
function accounts(address) external returns(address, uint256, uint256, uint256, uint256, uint256, uint256, uint256) envfree;
function startTime() external returns (uint256) envfree;
function currentEpoch() external returns (uint256) envfree;
}

function simplifyEpochProcessing(env e){
require e.block.timestamp == _stakeManager.startTime();
require _stakeManager.currentEpoch() == 0;
}

/* TODO: very usage of CONSTANT with Math.mulDiv or simplify mulDiv somehow, and replace simplifyEpochProcessing with reduceEpochProcessing

function reduceEpochProcessing(env e, uint256 maxEpochs) {
require e.block.timestamp >= _stakeManager.startTime();
uint256 currentEpoch = _stakeManager.currentEpoch();
uint256 newEpoch = _stakeManager.newEpoch(e);
require currentEpoch <= newEpoch;
require currentEpoch - newEpoch <= maxEpochs;
}

function reduceAccountProcessing(env e, address addr, uint256 maxEpochs) {
uint256 currentEpoch = _stakeManager.currentEpoch();
uint256 accountEpoch = getAccountEpoch(addr);
require accountEpoch <= currentEpoch;
require accountEpoch >= currentEpoch - maxEpochs;
}
*/

invariant MPcantBeGreaterThanMaxMP(address addr)
to_mathint(getAccountCurrentMultiplierPoints(addr)) <= to_mathint(getAccountMaxMultiplierPoints(addr))
filtered {
f -> f.selector != sig:migrateFrom(address,bool,StakeManager.Account).selector
}
{ preserved {
{ preserved with (env e) {
simplifyEpochProcessing(e);
/*reduceEpochProcessing(e, 3);
reduceAccountProcessing(e, addr, 3);*/
requireInvariant MaxMPIsNeverSmallerThanBalance(addr);
requireInvariant CurrentMPIsNeverSmallerThanBalance(addr);
}
Expand Down
7 changes: 0 additions & 7 deletions certora/specs/StakeManager.spec
Original file line number Diff line number Diff line change
Expand Up @@ -10,16 +10,9 @@ methods {
function _.migrateFrom(address, bool, StakeManager.Account) external => NONDET;
function _.increaseTotalMP(uint256) external => NONDET;
function _.migrationInitialize(uint256,uint256,uint256,uint256,uint256,uint256,uint256) external => NONDET;
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);
function _._ external => DISPATCH [] default NONDET;
}

function mulDivSummary(uint256 a, uint256 b, uint256 c) returns uint256 {
require c != 0;
return require_uint256(a*b/c);
}

function isMigrationfunction(method f) returns bool {
return
f.selector == sig:acceptUpdate().selector ||
Expand Down
1 change: 0 additions & 1 deletion certora/specs/StakeManagerProcessAccount.spec
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@ methods {
function totalStaked() external returns (uint256) envfree;
function totalMP() external returns (uint256) envfree;
function totalMPRate() external returns (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,uint256,uint256,uint256) external => NONDET;
Expand Down
1 change: 0 additions & 1 deletion certora/specs/StakeManagerStartMigration.spec
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,6 @@ methods {
function totalStaked() external returns (uint256) envfree;
function totalMP() external returns (uint256) envfree;
function previousManager() external returns (address) envfree;
function accounts(address) external returns(address, uint256, uint256, uint256, uint256, uint256, uint256, uint256) envfree;

function _.migrationInitialize(uint256,uint256,uint256,uint256,uint256,uint256,uint256) external => DISPATCHER(true);
function StakeManagerNew.totalStaked() external returns (uint256) envfree;
Expand Down
7 changes: 0 additions & 7 deletions certora/specs/StakeVault.spec
Original file line number Diff line number Diff line change
Expand Up @@ -7,16 +7,9 @@ methods {
function ERC20A.balanceOf(address) external returns (uint256) envfree;
function ERC20A.allowance(address, address) external returns(uint256) envfree;
function ERC20A.totalSupply() external returns(uint256) envfree;
function StakeManager.accounts(address) external returns(address, uint256, uint256, uint256, uint256, uint256, uint256, uint256) envfree;
function _.migrateFrom(address, bool, StakeManager.Account) external => DISPATCHER(true);
function _.increaseTotalMP(uint256) external => DISPATCHER(true);
function _.owner() external => DISPATCHER(true);
function Math.mulDiv(uint256 a, uint256 b, uint256 c) internal returns uint256 => mulDivSummary(a,b,c);
}

function mulDivSummary(uint256 a, uint256 b, uint256 c) returns uint256 {
require c != 0;
return require_uint256(a*b/c);
}

definition isMigrationFunction(method f) returns bool = (
Expand Down
15 changes: 15 additions & 0 deletions certora/specs/shared.spec
Original file line number Diff line number Diff line change
@@ -1,5 +1,15 @@
using StakeManager as _stakeManager;

methods {
function StakeManager.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);
}

function mulDivSummary(uint256 a, uint256 b, uint256 c) returns uint256 {
require c != 0;
return require_uint256(a*b/c);
}

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 ||
Expand Down Expand Up @@ -40,6 +50,11 @@ function getAccountLockUntil(address addr) returns uint256 {
return lockUntil;
}

function getAccountEpoch(address addr) returns uint256 {
uint256 epoch;
_, _, _, _, _, _, epoch, _ = _stakeManager.accounts(addr);
return epoch;
}

invariant MaxMPIsNeverSmallerThanBalance(address addr)
to_mathint(getAccountMaxMultiplierPoints(addr)) >= to_mathint(getAccountBalance(addr))
Expand Down

0 comments on commit 99c73be

Please sign in to comment.