2024-09-17 13:28:57 +02:00
|
|
|
import "./shared.spec";
|
|
|
|
|
2024-01-24 16:07:23 +01:00
|
|
|
using ERC20A as staked;
|
|
|
|
using StakeManagerNew as newStakeManager;
|
|
|
|
|
|
|
|
methods {
|
|
|
|
function staked.balanceOf(address) external returns (uint256) envfree;
|
2024-03-01 10:35:19 +01:00
|
|
|
function totalSupplyBalance() external returns (uint256) envfree;
|
|
|
|
function totalSupplyMP() external returns (uint256) envfree;
|
2024-06-19 11:26:03 +02:00
|
|
|
function previousManager() external returns (address) envfree;
|
2024-09-04 09:54:45 +02:00
|
|
|
function accounts(address) external returns(address, uint256, uint256, uint256, uint256, uint256, uint256, uint256) envfree;
|
2024-01-24 16:07:23 +01:00
|
|
|
|
2024-09-04 09:54:45 +02:00
|
|
|
function _.migrationInitialize(uint256,uint256,uint256,uint256,uint256,uint256,uint256) external => DISPATCHER(true);
|
2024-03-01 10:35:19 +01:00
|
|
|
function StakeManagerNew.totalSupplyBalance() external returns (uint256) envfree;
|
2024-01-24 16:07:23 +01:00
|
|
|
}
|
|
|
|
|
|
|
|
definition blockedWhenMigrating(method f) returns bool = (
|
|
|
|
f.selector == sig:stake(uint256, uint256).selector ||
|
|
|
|
f.selector == sig:unstake(uint256).selector ||
|
|
|
|
f.selector == sig:lock(uint256).selector ||
|
|
|
|
f.selector == sig:executeEpoch().selector ||
|
2024-09-25 12:53:59 -03:00
|
|
|
f.selector == sig:executeEpoch(uint256).selector ||
|
2024-03-01 10:56:19 +01:00
|
|
|
f.selector == sig:startMigration(address).selector ||
|
2024-09-04 09:54:45 +02:00
|
|
|
f.selector == sig:migrationInitialize(uint256,uint256,uint256,uint256,uint256,uint256,uint256).selector
|
2024-01-24 16:07:23 +01:00
|
|
|
);
|
|
|
|
|
|
|
|
definition blockedWhenNotMigrating(method f) returns bool = (
|
|
|
|
f.selector == sig:migrateTo(bool).selector ||
|
|
|
|
f.selector == sig:transferNonPending().selector
|
|
|
|
);
|
|
|
|
|
|
|
|
rule rejectWhenMigrating(method f) filtered {
|
2024-03-01 10:42:11 +01:00
|
|
|
f -> blockedWhenMigrating(f) && f.contract == currentContract
|
2024-01-24 16:07:23 +01:00
|
|
|
} {
|
|
|
|
calldataarg args;
|
|
|
|
env e;
|
|
|
|
|
|
|
|
require currentContract.migration != 0;
|
|
|
|
|
|
|
|
f@withrevert(e, args);
|
|
|
|
|
|
|
|
assert lastReverted;
|
|
|
|
}
|
|
|
|
|
|
|
|
rule allowWhenMigrating(method f) filtered {
|
|
|
|
f -> !blockedWhenMigrating(f)
|
|
|
|
} {
|
|
|
|
calldataarg args;
|
|
|
|
env e;
|
|
|
|
|
|
|
|
require currentContract.migration != 0;
|
|
|
|
|
|
|
|
f@withrevert(e, args);
|
|
|
|
|
|
|
|
satisfy !lastReverted;
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
rule rejectWhenNotMigrating(method f) filtered {
|
2024-03-01 10:42:11 +01:00
|
|
|
f -> blockedWhenNotMigrating(f) && f.contract == currentContract
|
2024-01-24 16:07:23 +01:00
|
|
|
} {
|
|
|
|
calldataarg args;
|
|
|
|
env e;
|
|
|
|
|
|
|
|
require currentContract.migration == 0;
|
|
|
|
|
|
|
|
f@withrevert(e, args);
|
|
|
|
|
|
|
|
assert lastReverted;
|
|
|
|
}
|
|
|
|
|
|
|
|
rule allowWhenNotMigrating(method f) filtered {
|
|
|
|
f -> !blockedWhenNotMigrating(f)
|
|
|
|
} {
|
|
|
|
calldataarg args;
|
|
|
|
env e;
|
|
|
|
|
|
|
|
require currentContract.migration == 0;
|
|
|
|
|
|
|
|
f@withrevert(e, args);
|
|
|
|
|
|
|
|
satisfy !lastReverted;
|
|
|
|
}
|
|
|
|
|
|
|
|
rule startMigrationCorrect {
|
|
|
|
env e;
|
|
|
|
address newContract = newStakeManager;
|
|
|
|
|
|
|
|
startMigration(e, newContract);
|
|
|
|
|
|
|
|
assert currentContract.migration == newContract;
|
2024-03-01 10:35:19 +01:00
|
|
|
assert newStakeManager.totalSupplyBalance() == currentContract.totalSupplyBalance();
|
2024-01-24 16:07:23 +01:00
|
|
|
}
|
|
|
|
|
2024-03-01 10:42:11 +01:00
|
|
|
rule migrationLockedIn(method f) filtered {
|
|
|
|
f -> !blockedWhenMigrating(f) && f.contract == currentContract
|
|
|
|
} {
|
2024-01-24 16:07:23 +01:00
|
|
|
env e;
|
|
|
|
calldataarg args;
|
|
|
|
|
|
|
|
require currentContract.migration != 0;
|
|
|
|
|
|
|
|
f(e, args);
|
|
|
|
|
|
|
|
assert currentContract.migration != 0;
|
|
|
|
}
|
|
|
|
|
2024-03-01 10:56:19 +01:00
|
|
|
rule epochStaysSameOnMigration(method f) filtered {
|
|
|
|
f -> !blockedWhenMigrating(f) && f.contract == currentContract
|
|
|
|
} {
|
2024-01-24 16:07:23 +01:00
|
|
|
env e;
|
|
|
|
calldataarg args;
|
|
|
|
|
|
|
|
uint256 epochBefore = currentContract.currentEpoch;
|
|
|
|
require currentContract.migration != 0;
|
|
|
|
|
|
|
|
f(e, args);
|
|
|
|
|
|
|
|
assert currentContract.currentEpoch == epochBefore;
|
|
|
|
}
|