Certora verification of the DLL

[QGarchery]

This PR completes the verification of the Double Linked List data-structure. It is done in two steps:

• the data-structure is abstracted into the usual DLL, and strong invariants are proved on this data-structure. Notably we prove that the DLL stays decreasingly sorted. Use ./certora/scripts/dll-simple.sh to run the verification.
• the data-structure from Morpho-Compound is verified, use ./certora/scripts/dll-fifo.sh to run the verification.

The specification files certora/specs/dll-simple.spec and certora/specs/dll-fifo.spec are organized as follows:

• definitions are given to make the specification clearer. For example the definition isTwoWayLinked is a predicate checking if the existence of a link from account A to account B implies the existence of the link from B to A.
• invariants and rules are proved using Certora. For example the invariant linkedIsInDLL states that an account that is linked to another account is necessarily in the double linked list. Notice that some of those invariants make heavy use interdependent invariants. The documentation about interdependent invariants was written in parallel of this work.
• derived results are "pen & paper" proved. This is to prove the most natural properties of the data-structure, without having to duplicate the invariants.

Here is the result of running the dll-fifo.sh script:

[MathisGD]

Didn't reviewed the specs, as I already approved them

[MathisGD]

Huge work, congrats again !