logos-co/staking
1
0
Fork 0
mirror of https://github.com/logos-co/staking.git synced 2025-01-11 11:14:45 +00:00
Code Issues Packages Projects Releases Wiki Activity

chore(StakeVault.spec): comment out purposefully failing rule

Browse Source 
This rule is only used for debugging purposes and serves no function for
production formal verification. Hence we're commenting it out.
This commit is contained in:
r4bbit 2024-03-04 10:12:41 +01:00
parent a90b730382
commit 50c8a11d5d
No known key found for this signature in database
GPG Key ID: E95F1E9447DC91A9
1 changed files with 5 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
certora/specs/StakeVault.spec
View File

@ -16,6 +16,10 @@ rule reachability(method f){
satisfy true;
}
/*
The rule below is commented out as it's merely used to easily have the
prover find all functions that change balances.
rule whoChangeERC20Balance(method f)
{
simplification();
@ -26,3 +30,4 @@ rule whoChangeERC20Balance(method f)
f(e,args);
assert before == staked.balanceOf(user);
}
*/