[Certora] Roles tree

[QGarchery]

This PR's goal is to verify that the following roles tree holds:

• owner >= curator
• curator >= allocator
• owner >= guardian

It does not verify that the inequalities are strict