Right now, the contract keeps track of a user's and a global potentialMP
potentialMP is the MP left to mint globally and for individual users until they reach their max amount.
Therefore, when userMP and totalMP is increase, potentialMP and user.potentialMP will decrease accordingly (unless stake() is called in which case potentialMP can increase again).
While this works, it turns out to be rather tricky to formally verify that an accountMPLessEqualMaxMP because we don't have any way to easily check what the maxMP is (again potentialMP is not representative because it decreases with time).
So we decided to move away from potentialMP and simply have maxMP which can only increase and be queried at any time.
Right now, the contract keeps track of a user's and a global
potentialMPpotentialMPis the MP left to mint globally and for individual users until they reach their max amount. Therefore, whenuserMPandtotalMPis increase,potentialMPanduser.potentialMPwill decrease accordingly (unlessstake()is called in which casepotentialMPcan increase again).While this works, it turns out to be rather tricky to formally verify that an
accountMPLessEqualMaxMPbecause we don't have any way to easily check what themaxMPis (againpotentialMPis not representative because it decreases with time).So we decided to move away from
potentialMPand simply havemaxMPwhich can only increase and be queried at any time.