[Certora] Created obligations

[QGarchery]

See description of the rules.

This verification will not go through after #367, but it can be adapted (modulo some summary)

[bhargavbh]

LGTM.
potentially we also are interested that obligation can be created only by touchObligation, take, withdraw, repay, supplyCollateral, withdrawCollateral, liquidate: Prover Link

rule onlyTouchObligationCreates(env e, method f, calldataarg args, bytes20 id)
filtered { f -> f.selector != sig:touchObligation(MorphoV2.Obligation).selector
                || f.selector != sig:take(uint256,uint256,uint256,uint256,address,address,bytes,address,MorphoV2.Offer,MorphoV2.Signature,bytes32,bytes32[]).selector
                || f.selector != sig:withdraw(MorphoV2.Obligation,uint256,uint256,address,address).selector
                || f.selector != sig:repay(MorphoV2.Obligation,uint256,address).selector
                || f.selector != sig:supplyCollateral(MorphoV2.Obligation,uint256,uint256,address).selector
                || f.selector != sig:withdrawCollateral(MorphoV2.Obligation,uint256,uint256,address,address).selector
                || f.selector != sig:liquidate(MorphoV2.Obligation,uint256,uint256,uint256,address,bytes).selector
        } {
    require !MorphoV2.obligationCreated(id);
    f(e, args);
    assert !MorphoV2.obligationCreated(id);
}

The roundtrip property (toObligation(toId(obligation)) == obligation ) also is interesting but involves a lot more summarise. can be proved later.

[MathisGD]

LGTM except one question on one rule

[QGarchery]

This was the only function that was changing the state before the obligation is created. Without this require, the fee would switch back to the default fees when the obligation will indeed be created