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

fix(StakeManager.spec): ensure `revertsWhenNoMigration` passes 

The were changes in the contracts that caused this rule to fail.
Namely `migrateTo` shouldn't be reverting so this as been removed from
the rule and `transferNonPending` has been added as it was missing.
This commit is contained in:
r4bbit 2024-03-04 16:19:45 +01:00 committed by Ricardo Guilherme Schmidt
parent e723464245
commit e9f0077488
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
certora/specs/StakeManager.spec
View File

@ -27,8 +27,8 @@ function getAccountBalance(address addr) returns uint256 {
function isMigrationfunction(method f) returns bool {
return
f.selector == sig:migrateFrom(address,bool,StakeManager.Account).selector ||
f.selector == sig:migrateTo(bool).selector;
f.selector == sig:migrateTo(bool).selector ||
f.selector == sig:transferNonPending().selector;
}
/* assume that migration is zero, causing the verification to take into account only