[Certora] Liquidate buffer, with executable code

[QGarchery]

This verification is meant to show that if liquidation happen with LTV < 1 / LIF (note that 1 / LIF > LLTV by design), then this liquidation is healthy in the following sense: the position's health factor increases. This means that liquidation happening in the buffer [LLTV, 1/LIF] always lead to healthy positions, if liquidating multiple times, and don't lead to bad debt

[QGarchery]

It seems very difficult to make this verification go though. Here is an example of such run, but deviating a little bit from it seems to cause a timeout. Also this run requires some heavy modifications:

• passing the LIF to the liquidate function
• munging to not update the value of repaidAssets
• munging to comment out _accrueInterest (even though it should be skipped given the assumptions)
• munging to require that no bad debt is realized (even though it should be provable by the assumptions)

For these reasons, it seems prefereable to do #710

[QGarchery]

A new trick (see 9ee0ccf) is making the verification much faster for the prover. So now this PR is considered over #710

[colin-morpho]

Blazing fast, hard to believe it could ever timeout.