[Certora] settlement fee spread assumption

[QGarchery]

Fixes:

• [Certora] side effect of calling settlementFee in a rule #932

Also:

• removes occurrences of onRatify (now renamed isRatified)
• make settlementFeeSpread use havoc all by default

[QGarchery]

I tried this

Suggested change

	uint256 fee = settlementFee(id, timeToMaturity);
	touchMarket(e, offer.market);
	uint256 fee = settlementFee@withrevert(id, timeToMaturity);
	assert !lastReverted;

but it was causing a long running time in this run. Also it wasn't proving exactly that it's not pruning meaningful paths, because storeInCode is summarized to not revert in this file

[QGarchery]

as is, it feels like TouchMarketIsCalled.spec is a bit redundant with the marketIsCreatedAfter* rules, but it's actually not proving exactly the same thing

[jhoenicke]

would it work to call settlementFee after take or does the take change the settlementFee?

After take it should not revert, right?

[jhoenicke]

I tried calling settlementFee after and the HAVOC_ALL summary of the callbacks set tickSpacing to 0 😦

With HAVOC_ECF it works, though.

[QGarchery]

Yes basically we can either:

• have it before which uses havoc all by default, but there is this question of whether it prunes a path
• have it after which requires to have havoc ecf for all callbacks

I like the first solution better, since it has no unrelated assumptions about callbacks (you need to prove something about the settlement fee, which makes sense since this rule is about settlement fee)

[jhoenicke]

The TouchMarketIsCalled looks fine, the rest is just a comment update.