r4bbit e5d9a451e7 fix(specs): make `sumOfMultiplierPointsIsMultiplierpoints` work again ... This invariant failed as the prover started making wrong assumptions about the relationship between anyone's account's `totalMP` and its `balance`, as well as an account's `bonusMP` and its `balance`. This commit fixes it by adding the necessary invariants to proof the property.		2024-10-12 17:38:44 -03:00
..
MaxMPRule.spec	refactor(certora): move rule about MP not greater than max MP into own	2024-10-08 10:14:20 -03:00
StakeManager.spec	fix(specs): make `sumOfMultiplierPointsIsMultiplierpoints` work again	2024-10-12 17:38:44 -03:00
StakeManagerProcessAccount.spec	fix(certora): exclude `stake()` from rule that checks account balance	2024-10-12 17:38:43 -03:00
StakeManagerStartMigration.spec	refactor(StakeManager): optimize epoch finalization and execution of accounts and epochs	2024-09-26 15:41:35 -03:00
StakeVault.spec	refactor(certora): introduce shared.spec to reuse helper functions	2024-09-19 14:35:08 +02:00
shared.spec	refactor(certora): move rule about MP not greater than max MP into own	2024-10-08 10:14:20 -03:00