Closed 0x-r4bbit closed 1 month ago
These invariants should be ported over:
initialMPIsNeverSmallerThanBalance
userMPIsNeverSmallerThanInitialMP
MPcantBeGreaterThanMaxMP
^ This one we can't actually do because we don't keep track of initial MP (and we don't need to)
initial
These invariants should be ported over:
initialMPIsNeverSmallerThanBalance
-userMPIsNeverSmallerThanInitialMP
MPcantBeGreaterThanMaxMP