Formal verification wish list

[QGarchery]

todo:

• [midnight] (WIP, see [Certora] midnight tokens #10) can't exploit the bundler allowance, see this comment
• [midnight] show that the token balances of MidnightBundles cannot go down, assuming MIDNIGHT is correctly set (so it cannot pull tokens)
• [midnight] show that a market isn't read before it is created
• [blue] prove that migrating borrow positions leave no residue (see this comment)