Add certora rule that ensures correct MP estimation for any given stake time

[0x-r4bbit]

For any amount of tokens deposited, within any moment of contract life cycle, process account and process epoch creates valid outputs.

Something like:

{ random amount of account creation with random amount of deposit stake & lock time }
{ random amount of time have been passed }
{ random amount of account creation with random amount of deposit stake & lock time }
{ random calls to StakeManager.processAccount}
{ random amount of account creation with random amount of deposit stake & lock time }
{ random calls to StakeManager.processAccount}

[0x-r4bbit]

This one turns out to be hard to figure out.

Also there's some effort going on in https://github.com/vacp2p/staking-reward-streamer that we'll likely leverage, which will have an impact on the staking contract's functions (and inherently its rules).

I'm holding off with this one until after we've done #116