refactor(StakeManager): optimize stake, account init and lock function

[3esmit]

Description

This pull request focuses solely on cleaning up the code. The clean-up removes outdated or unnecessary code, which was masking a bug that is being addressed in #127

Details

This changes the account initialization on stake():

• removing zombie instructions, inherited from restaking ability which was removed:
  • account was having bonusMP += and totalMP +=, but these values were always zero;
• making it more clear, by removing _mintBonusMP, and initializing account on a single write;
• allowing the StakeVault to be recycled after unstaking all funds, by removing the check for lockUntil != 0

This changes the method lock():

• making it more clear, by removing _mintBonusMP
• fixing a bug which was updating lastMint on lock()->_mintBonusMP to current block.timestamp(), which shouldnt be updated to that value, masking the bug addressed in fix(StakeManager): fix finalizeEpoch to use last epoch epochEnd #127

Details on #127 bug

The bug was hidden because the _mintBonusMP function contained a line that updated account.lastMint to the same value as startEpoch. This had the unintended effect of making the epoch estimation appear correct when calling StakeManager.lock(). As a result, the underlying bug wasn’t detected in test_UpdateLockupPeriod.

PR #130 does not fix this bug; instead, it cleans up the code that was hiding it for test_UpdateLockupPeriod to cach it. The actual bug fix is handled in PR #127, which also introduces other tests that would have catched it while implementing the multiplier points estimation.

Purpose

Code Cleanup: This PR removes code that was masking the bug, allowing the system to function properly moving forward.
Not a Bug Fix: It doesn't directly fix the bug but removes the part of the code that was preventing the issue from being caught in the test.

Important Notes

The test failures seen in executeAccount->processAccount->mintMP are unrelated to this cleanup. However, PR #130 requires that PR #127 and PR #129 be merged first to ensure proper function.

Checklist

Ensure you completed all of the steps below before submitting your pull request:

• Added natspec comments?
• Ran forge snapshot?
• Ran pnpm gas-report?
• Ran pnpm lint?
• Ran forge test?
• Ran pnpm verify?

[0x-r4bbit]

Changes look good to me, but it seems this is not passing tests

[3esmit]

Updated description to explain exactly whats happening here, why this tests are failing for this correct code change.

[3esmit]

So this PR is failing on verify because the spec is outdated.

Two things are failing:

• The current spec considers restaking is possible (why it didn't failed earlier, btw?)
  What is failing is that is havocing inside account, adding some random multiplier points, and see if it incrases (in stake function). However, now the staking contract dont allow restake, and it should not increase anymore.
  Here I tested a change in this code where it would add the old balance back again https://prover.certora.com/output/585415/7c5efd9e4bbf4d889c36e9acaada8ee6?anonymousKey=303a179377435cf7b148f082d0a45e0380ddde64
  I need @0x-r4bbit some input here on how to update this spec

• The other reason I still didn't figured out (just had time to dig into the one above). It's really strange, because it's saying that is possible that stake function to set the account.epoch > than the currentEpoch.
  https://prover.certora.com/output/585415/288f4d626b9f412f8f7f78ec6ce440d7?anonymousKey=36b7b0f8ffdb668e596fed82647c213fce66f774
  I'll figure this one out tomorrow, and than we see how to update the spec (or fix the contract).
  @0x-r4bbit if you see something let me know, but you don't have to look into this one yet because I didn't spent time with it yet.

[0x-r4bbit]

@3esmit I added a commit here with these changes:

• adds an accountBonusMPIsZeroIfBalanceIsZero invariant (prover run: https://prover.certora.com/output/6199/d6ef43d62ee34413840f6750a6ee64e4?anonymousKey=8f051bae33f9184ab91bc5538afc4d416d2a88ee)
• adds that invariant and the accountCurrentMPIsZeroIfBalanceIsZero invariant to the failing sumOfMultiplierPointsIsMultiplierPoints invariant, which then passes (prover run: https://prover.certora.com/output/6199/ecd475b011ad48008f5b0529fb110c46?anonymousKey=122620db726e46da2696bf1b8eb97fdfa7b1ce9d)

This should do the trick