Improve assumptions in AllocateDeallocateInputValidation spec

Recover the `decreaseTimelock` case once it is fixed in CVL

Permanent Interest Freeze via maxRate and elapsed Manipulation

Fee Accrual Dilution via accrueInterestView Rounding Asymmetry

prove expected bound

Improve properties about marketIds

Struct interface of market adapter

Recursive initialization of git submodules fail

I'm wondering if this issue is not more pervasive than we think, and it would be best to isolate by default. I'm thinking that wanting to have operations be in the same tx should be explicit (with a multicall, it's the rare case)

[Certora] prove pendingCount