abs and safeAbs verification + CVL2 migration

[github-actions[bot]]

Changes to gas cost

Generated at commit: 2fada28e702bd3b0197d11c1a5e7ecec6a0cbe16, compared to commit: 9fc9b2a1a40463f4fa26f547fd76458a73ac6cbb

🧾 Summary (20% most significant diffs)

Contract	Method	Avg (+/-)	%
MathMock contract	log2	+91 ❌	+19.12%

---

Full diff report 👇

| Contract | Deployment Cost (+/-) | Method | Min (+/-) | % | Avg (+/-) | % | Median (+/-) | % | Max (+/-) | % | # Calls (+/-) | |:-|-:|:-|-:|-:|-:|-:|-:|-:|-:|-:|-:| | **MathRef contract** | 238,081 (+37,836) | _divUp_
_log2Dichotomy_
_log2Naive_
_max_
_min_
_zeroFloorSub_ | 573 (-26)
4,741 (-54)
44,490 (-538)
376 (+63)
408 (+63)
416 (-26) | **-4.34%**
**-1.13%**
**-1.19%**
**+20.13%**
**+18.26%**
**-5.88%** | 573 (-26)
4,741 (-54)
44,490 (-538)
376 (+63)
408 (+63)
416 (-26) | **-4.34%**
**-1.13%**
**-1.19%**
**+20.13%**
**+18.26%**
**-5.88%** | 573 (-26)
4,741 (-54)
44,490 (-538)
376 (+63)
408 (+63)
416 (-26) | **-4.34%**
**-1.13%**
**-1.19%**
**+20.13%**
**+18.26%**
**-5.88%** | 573 (-26)
4,741 (-54)
44,490 (-538)
376 (+63)
408 (+63)
416 (-26) | **-4.34%**
**-1.13%**
**-1.19%**
**+20.13%**
**+18.26%**
**-5.88%** | 1 (0)
1 (0)
1 (0)
1 (0)
1 (0)
1 (0) | | **MathMock contract** | 147,190 (+43,637) | _divUp_
_log2_
_max_
_zeroFloorSub_ | 372 (+34)
567 (+91)
401 (+67)
405 (+22) | **+10.06%**
**+19.12%**
**+20.06%**
**+5.74%** | 454 (+34)
567 (+91)
401 (+67)
405 (+22) | **+8.10%**
**+19.12%**
**+20.06%**
**+5.74%** | 475 (+34)
567 (+91)
401 (+67)
405 (+22) | **+7.71%**
**+19.12%**
**+20.06%**
**+5.74%** | 475 (+34)
567 (+91)
401 (+67)
405 (+22) | **+7.71%**
**+19.12%**
**+20.06%**
**+5.74%** | 5 (0)
2 (0)
1 (0)
1 (0) |

[QGarchery]

What's the goal of this PR? What issue is it trying to solve pls?

The migration to CVL2 is today. We can still use CVL1 but it's getting deprecated, and so it will be difficult to maintain in the future. I'm starting to work on the translation of our specs to CVL2 for that reason, and also because there is one bug fix that we need to prove the properties of the abs functions (it has to do with the negation of mathematical integers)

I infer that CVL2 requires not defining functions in specs?

You can define functions in specs in CVL2 but there is an issue with the definition of MIN_INT256. It seems to come from a check that prevents creating signed integers that are too big or too small, I'm still investigating

[QGarchery]

Closing this in favor of https://github.com/morpho-org/morpho-utils/pull/109, where we don't try to also add new rules