Listing Safe Assumptions
Todo
Write a method that requires all the safe assumptions, just add it in all your rules and preserved blocks.
function safeAssumptions(env e) {
require e.msg.sender != 0;
// assumption justified because we assume the token isn't in circulation
require closed() => balance() == 0;
requireInvariant foo(e);
requireInvariant bar();
}
invariant foo(env e)
...
{ { preserved with (env e2) { safeAssumptions(e2); } } }
invariant bar()
...
{ { preserved with (env e2) { safeAssumptions(e2); } } }
rule baz() {
env e;
safeAssumptions(e);
...
}