FV: Verify which function can make which state changes

[mmv08]

Similar to our specs in the safe-smart account, we can write a few rules around which state changes are allowed to which functions.

Example of such specs:
https://github.com/safe-global/safe-smart-account/blob/499b17ad0191b575fcadc5cb5b8e3faeae5391ae/certora/specs/Safe.spec#L134-L147

A couple of ideas:

• A recovery was started state change detected -> executeRecovery was called
• New guardian added -> addGuardianWithThreshold was called
• ... so on and so forth

[nlordell]

I would suggest to have multiple rules of the form:

rule XOnlyChangesWithY(method f, env e) {
    type xBefore = currentContract.x;
    f(e);
    type xAfter = currentContract.x;
    
    assert xBefore != xAfter => f.selector == Y.selector;
}

Example from @mmv08: https://github.com/safe-global/safe-smart-account/blob/499b17ad0191b575fcadc5cb5b8e3faeae5391ae/certora/specs/Safe.spec#L84-L97