Add support for formal verification tools

[nielstron]

Nagini is a formal verification tool that is able to analyze python. It can be used to annotate existing contract functions, which would simply be ignored by the opshin compiler. Further, it needs to be checked whether Nagini can be tweaked to support the used dataclasses, as well as whether the threading logic can be used to leverage a temporal-logic style analysis of the smart contracts in context.

• allow import of nagini contract primitives --> not executable anyways, needs to be removed by rewriting
• check support for dataclasses
• explore temporal-logic style analysis using Nagini

Further references are in the wiki: https://github.com/marcoeilers/nagini/wiki

[nielstron]

Another alternative for formal verification could be employing deal

• allow import of deal contract primitives
• check support for dataclasses