[Certora] Precise calculation of earliestExecutionTime()

[jhoenicke]

This fixes the spec EarliestTime and tracks the minDecreaseTimelock values precisely.

I still get a counterexample when for decreaseTimelock(). Apparently there is something strange in the prover, as the counterexample doesn't even enter the if statement in the hook.

Disclaimer: I also noticed that the traces for the sanity check are wrong, in the sense that they compute the signature incorrectly. It looks like this problem already existed before. I opened a ticket for the Certora prover to investigate this.

[jhoenicke]

I now believe that the only reason why the current code verifies (even the current main branch) is because the loop unrolling depth is too low for extractDecreaseTimelockArgs. Unfortunately the sanity check doesn't catch this, because it generates traces where the signature is never decreaseTimelock() even for the decreaseTimelock function.