[Certora] Reentrancy

[QGarchery]

This PR's goals is to prove that there is no possibility of a reentrancy attacks, assuming that:

• Tokens are trusted. This assumption could potentially be relaxed, based on the fact that the accounting does not depend on reentrant calls. In fact, MetaMorpho has been built with this concern in mind, notably to take into account ERC777 tokens. To simplify the verification though, tokens are assumed to not reenter the contract.
• Morpho Blue and Morpho Blue markets are trusted. Morpho Blue is an immutable contract, and thoroughly verified.

Note also that both assumption make sense in the context of timelocked markets: a market (and its corresponding collateral and loan token) can only be added after going through a timelock phase. After a proper analysis during this period, a market could be considered safe